OAI/NumberTheory/CubicGauss/Reciprocity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Frobenius identities and cubic reciprocity over Eisenstein integers.

  1. lemma OAI.CubicFirstMoment.ReciprocityKernel.gaussSum_card_frobenius line 16

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:19 (same declaration text).

  2. theorem OAI.CubicFirstMoment.ReciprocityKernel.cubic_jacobi_card_relation line 38

    Distinct definitions of this name: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:39 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.ReciprocityKernel.cubic_jacobi_card_relation@path.

  3. lemma OAI.CubicFirstMoment.omegaE_primitive line 104

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:105 (same declaration text).

  4. lemma OAI.CubicFirstMoment.cubeRoot_reduce_inj line 108

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:109 (same declaration text).

  5. lemma OAI.CubicFirstMoment.cubicResidueCharE_cube line 117

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:118 (same declaration text).

  6. lemma OAI.CubicFirstMoment.cubicResidueCharE_neg_one line 127

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:128 (same declaration text).

  7. lemma OAI.CubicFirstMoment.cubicResidueCharE_value_cube line 135

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:136 (same declaration text).

  8. lemma OAI.CubicFirstMoment.cubicResidueCharE_ringHomComp_ne_one line 144

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:145 (same declaration text).

  9. lemma OAI.CubicFirstMoment.primeJacobi_eq_sumE line 160

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:161 (same declaration text).

  10. lemma OAI.CubicFirstMoment.normNat_cast_eq_mul_conjugate line 167

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:168 (same declaration text).

  11. lemma OAI.CubicFirstMoment.cubic_reciprocity_frobenius line 175

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:175 (same declaration text).

  12. theorem OAI.CubicFirstMoment.cubic_reciprocity_distinct_char line 235

    Also declared: OAI/NumberTheory/CubicGram/ReciprocityKernel.lean:234 (same declaration text).

  13. lemma OAI.CubicFirstMoment.primary_of_mul line 252

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:17 (same declaration text).

  14. lemma OAI.CubicFirstMoment.primary_induction line 257

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:22 (same declaration text).

  15. lemma OAI.CubicFirstMoment.primary_one line 289

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:54 (same declaration text).

  16. lemma OAI.CubicFirstMoment.cubicSymbol_one_lower line 291

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:56 (same declaration text).

  17. lemma OAI.CubicFirstMoment.cubicSymbol_neg line 294

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:59 (same declaration text).

  18. lemma OAI.CubicFirstMoment.cubicSymbol_conjugate line 305

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:70 (same declaration text).

  19. lemma OAI.CubicFirstMoment.reciprocity_of_prime_divisor_relation line 318

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:83 (same declaration text).

  20. lemma OAI.CubicFirstMoment.same_char_primary_primes line 334

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:99 (same declaration text).

  21. lemma OAI.CubicFirstMoment.cubic_reciprocity_conjugate line 361

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:124 (same declaration text).

  22. theorem OAI.CubicFirstMoment.cubic_reciprocity_prime line 419

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:181 (same declaration text).

  23. theorem OAI.CubicFirstMoment.cubic_reciprocity line 429

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:189 (same declaration text).

  24. theorem OAI.CubicFirstMoment.gauss_twisted_mul line 457

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:215 (same declaration text).

  25. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_sq_eq_star line 461

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:219 (same declaration text).

  26. lemma OAI.CubicFirstMoment.cubicSymbol_sq_eq_star line 470

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:228 (same declaration text).

  27. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_eq_zero_of_dvd line 480

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:238 (same declaration text).

  28. lemma OAI.CubicFirstMoment.cubicSymbol_eq_zero_of_not_isCoprime line 487

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:245 (same declaration text).

  29. theorem OAI.CubicFirstMoment.gauss_mul line 504

    Also declared: OAI/NumberTheory/CubicGram/Reciprocity.lean:261 (same declaration text).