ModuleSimpleRootFactorization.lean
Nyll.ValuedFieldTheory.Valuation.Henselian.SimpleRootFactorization
2 declarations indexed from sourceView source ↗ Module documentation
From simple-root Hensel lifting to valuation factorization
The Henselian ring assumption now supplies the actual coprime factors. The valuation factorization criterion then extends the monic result to all primitive polynomials, with the prescribed reductions and degree bounds.
Declarations
DiscreteValuationField.monicResidualCoprimeFactorLifting_of_henselianRing
DocumentationThe simple-root Henselian condition supplies monic coprime-factor lifting.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
variable {K : Type*} [Field K] (V : ValuationSubring K)
[HenselianRing V (IsLocalRing.maximalIdeal V)]
DiscreteValuationField.henselFactorization_of_henselianRing
DocumentationA Henselian valuation ring satisfies the full primitive factorization form of Hensel's lemma, without completeness or rank assumptions.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
variable {K : Type*} [Field K] (V : ValuationSubring K)
[HenselianRing V (IsLocalRing.maximalIdeal V)]