OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of the unit, ramified exponent and primary coordinates needed to define the cubic theta coefficients without choices of associates.

  1. lemma OAI.CubicFirstMoment.primary_lambda_emultiplicity line 11
  2. lemma OAI.CubicFirstMoment.unit_lambda_emultiplicity line 17
  3. theorem OAI.CubicFirstMoment.unit_ramified_primary_unique line 24

    Source documentation

    The published decomposition is unique after imposing primarity.

    theorem unit_ramified_primary_unique {u u' : Eisensteinˣ} {k k' : ℕ}
    {a a' : Eisenstein} (ha : primary a) (ha' : primary a')
    (he : (u:Eisenstein)*lambdaE^k*a = (u':Eisenstein)*lambdaE^k'*a') :
    u = u' ∧ k = k' ∧ a = a' := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.lambdaE