OAI/NumberTheory/CubicMoment/Estimates/CubicNumeratorNoncube.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every noncube numerator defines a nonprincipal cubic character. The proof keeps ramification and cube-factor deletions explicit.

  1. lemma OAI.CubicFirstMoment.nonprincipal_transport line 10
  2. lemma OAI.CubicFirstMoment.mixed_ramified_cubic_nonprincipal line 16
  3. theorem OAI.CubicFirstMoment.cubicNumeratorChar_noncube line 50

    Source documentation

    Nonprincipality for the full numerator, with no squarefreeness, primarity, unit, or ramification restrictions.

    theorem cubicNumeratorChar_noncube (hpub : CubicSupplementaryPeriodicity)
    {v : Eisenstein} (hv : v ≠ 0) (hn : ¬∃ j : Eisenstein, j^3=v) :
    cubicNumeratorChar hpub v hv ≠ 1 := by
…

    Mentions: OAI.CubicFirstMoment.CubicSupplementaryPeriodicity, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicNumeratorChar

  4. theorem OAI.CubicFirstMoment.cubicNumeratorChar_eq_one_iff_cube line 80