RamifiedUnit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The unit factor in a ramified polynomial relation

The exact constant coefficient, together with divisibility of the other nonleading coefficients, gives a factor with constant coefficient one. At a root in the maximal ideal this factor is a unit.

theorem OAI.CirculantHadamard.RamifiedUnit.exists_polynomial_unit_factor line 29

Source documentation

The polynomial form of the unit factor in an Eisenstein relation.

theorem exists_polynomial_unit_factor (f : R[X]) (a : R) (ha : a ≠ 0)
    (hf : f.Monic) (hdeg : 0 < f.natDegree) (hzero : f.coeff 0 = a)
    (hcoeff : ∀ i < f.natDegree, a ∣ f.coeff i) :
    ∃ q : R[X], f = X ^ f.natDegree + C a * (1 + X * q) := by
…

theorem OAI.CirculantHadamard.RamifiedUnit.exists_unit_mul_root_pow line 64

Source documentation

A root in the maximal ideal turns the normalized polynomial factor into a unit, and therefore expresses the constant coefficient as a unit times the ramified power.

theorem exists_unit_mul_root_pow (f : R[X]) (a : R) (ha : a ≠ 0)
    (hf : f.Monic) (hdeg : 0 < f.natDegree) (hzero : f.coeff 0 = a)
    (hcoeff : ∀ i < f.natDegree, a ∣ f.coeff i)
    (z : S) (hz : z ∈ IsLocalRing.maximalIdeal S) (hroot : aeval z f = 0) :
    ∃ u : Sˣ, algebraMap R S a = (u : S) * z ^ f.natDegree := by
…