CyclotomicFactorDivision.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A projected factor is integrally divisible by the residue prime

The primitive-character values live in the actual cyclotomic quotient. Their product is evaluated from the actual group-ring product. The DVR inequality chooses a factor, and the monic remainder theorem transfers its divisibility to the smaller cyclic group ring.

theorem OAI.CirculantHadamard.LocalComparison.projected_factor_divisible line 28

Source documentation

The ramified DVR and its value of p imply the concrete choice of a divisible projected factor. These are local-ring properties, independent of the input factors. The scalar and group exponents are both e + 2.

theorem projected_factor_divisible {p e D : ℕ} [NeZero p] (hp : p.Prime)
    [IsDomain (AdjoinRoot (cyclotomic (p ^ (e + 2)) A))]
    [IsDiscreteValuationRing (AdjoinRoot (cyclotomic (p ^ (e + 2)) A))]
    (hpS : (p : AdjoinRoot (cyclotomic (p ^ (e + 2)) A)) ≠ 0)
    (hD : 0 < D)
    (hpval : addVal (AdjoinRoot (cyclotomic (p ^ (e + 2)) A))
      (p : AdjoinRoot (cyclotomic (p ^ (e + 2)) A)) = (D : ℕ∞))
    (b : Aˣ) (F K : Elem A (p ^ (e + 2)))
    (hFK : F * K = scalar (p ^ (e + 2)) ((p : A) ^ (e + 2) * (b : A))) :
    (∃ F', cyclicProjection A (pow_dvd_pow p (Nat.le_succ (e + 1))) F =
      scalar (p ^ (e + 1)) (p : A) * F') ∨
    (∃ K', cyclicProjection A (pow_dvd_pow p (Nat.le_succ (e + 1))) K =
…