OAI/NumberTheory/CubicGram/Definitions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Primary Eisenstein elements, residue characters, Gauss sums and first-moment target definitions.

  1. def OAI.CubicFirstMoment.omega line 16

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:16 (same declaration text).

  2. def OAI.CubicFirstMoment.eisensteinRing line 18

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:18 (same declaration text).

  3. abbrev OAI.CubicFirstMoment.Eisenstein line 19

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:19 (same declaration text).

  4. def OAI.CubicFirstMoment.omegaE line 21

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:21 (same declaration text).

  5. def OAI.CubicFirstMoment.norm line 24

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:24 (same declaration text).

  6. def OAI.CubicFirstMoment.normNat line 26

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:26 (same declaration text).

  7. def OAI.CubicFirstMoment.primary line 28

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:28 (same declaration text).

  8. def OAI.CubicFirstMoment.primaryPrime line 30

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:30 (same declaration text).

  9. def OAI.CubicFirstMoment.modulus line 32

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:32 (same declaration text).

  10. abbrev OAI.CubicFirstMoment.Residues line 34

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:34 (same declaration text).

  11. def OAI.CubicFirstMoment.residueRepresentative line 36

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:36 (same declaration text).

  12. def OAI.CubicFirstMoment.cubicSymbolAtPrime line 39

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:39 (same declaration text).

  13. def OAI.CubicFirstMoment.additivePhase line 48

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:48 (same declaration text).

  14. def OAI.CubicFirstMoment.gaussAtPrime line 52

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:52 (same declaration text).

  15. def OAI.CubicFirstMoment.cStar line 58

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:58 (same declaration text).

  16. def OAI.CubicFirstMoment.primeCutoffSum line 60

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:60 (same declaration text).

  17. def OAI.CubicFirstMoment.firstMomentScale line 63

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:63 (same declaration text).

  18. def OAI.CubicFirstMoment.FirstMomentStatement line 65

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:65 (same declaration text).

  19. def OAI.CubicFirstMoment.theta line 71

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:71 (same declaration text).

  20. def OAI.CubicFirstMoment.AngularComparisonStatement line 73

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:73 (same declaration text).

  21. def OAI.CubicFirstMoment.AngularCancellationStatement line 79

    Also declared: ComparatorChallenges/PattersonFirstMoment.lean:79 (same declaration text).