OAI/NumberTheory/CubicMoment/Estimates/PrimaryHeckeCharacter.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The actual finite character attached to the primary mixed cubic symbol. Including the modulus 3 makes primary normalization periodic and removes its dependence on the choice of a unit associate.

  1. lemma OAI.CubicFirstMoment.isCoprime_of_residue_isUnit line 15

    Distinct definitions of this name: OAI/NumberTheory/CubicGauss/CubicFourier.lean:49 (different declaration text). Qualify references as OAI.CubicFirstMoment.isCoprime_of_residue_isUnit@path.

  2. lemma OAI.CubicFirstMoment.primaryNormalize_mul_of_residue_units line 26
  3. lemma OAI.CubicFirstMoment.primaryNormalize_unit line 36
  4. def OAI.CubicFirstMoment.primaryMixedLift line 40
  5. lemma OAI.CubicFirstMoment.primaryMixedLift_primary line 44
  6. lemma OAI.CubicFirstMoment.primaryMixedLift_one line 49
  7. lemma OAI.CubicFirstMoment.primaryMixedLift_mul line 53
  8. lemma OAI.CubicFirstMoment.primaryMixedLift_unit line 63
  9. lemma OAI.CubicFirstMoment.primaryMixedLift_congr_parts line 68
  10. lemma OAI.CubicFirstMoment.primaryMixedLift_congr line 89
  11. lemma OAI.CubicFirstMoment.primaryMixedLift_nonunit line 98
  12. def OAI.CubicFirstMoment.primaryMixedResidueChar line 117

    Source documentation

    The finite residue character agrees with the actual mixed cubic symbol on primary elements and is trivial on global units. It may still be imprimitive; conductor reduction is a separate step.

    def primaryMixedResidueChar (a b : Eisenstein) (ha : primary a) (hb : primary b) :
    MulChar (Residues (3*(a*b))) ℂ where
…

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

  13. lemma OAI.CubicFirstMoment.primaryMixedResidueChar_mk line 134
  14. lemma OAI.CubicFirstMoment.primaryMixedResidueChar_primary line 139
  15. lemma OAI.CubicFirstMoment.primaryMixedResidueChar_trivialInfinity line 144
  16. lemma OAI.CubicFirstMoment.primaryMixedLift_norm_le_one line 151
  17. lemma OAI.CubicFirstMoment.primaryMixedLift_associated line 160
  18. lemma OAI.CubicFirstMoment.star_primaryMixedLift line 166
  19. def OAI.CubicFirstMoment.primaryMixedIdealChar line 172

    Source documentation

    The actual ideal coefficient, with ramified factors explicitly zero.

    def primaryMixedIdealChar (a b : Eisenstein) (ν : EisensteinIdealExponent) : ℂ :=
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent

  20. lemma OAI.CubicFirstMoment.primaryMixedIdealChar_add line 175
  21. lemma OAI.CubicFirstMoment.primaryMixedIdealChar_at_element line 181
  22. lemma OAI.CubicFirstMoment.primaryMixedIdealChar_norm_le_one line 188
  23. lemma OAI.CubicFirstMoment.star_primaryMixedIdealChar line 192