OAI/NumberTheory/CubicGram/Reciprocity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Full cubic reciprocity and twisted multiplicativity of Gauss sums.

  1. lemma OAI.CubicFirstMoment.primary_of_mul line 17

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:252 (same declaration text).

  2. lemma OAI.CubicFirstMoment.primary_induction line 22

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:257 (same declaration text).

  3. lemma OAI.CubicFirstMoment.primary_one line 54

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:289 (same declaration text).

  4. lemma OAI.CubicFirstMoment.cubicSymbol_one_lower line 56

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:291 (same declaration text).

  5. lemma OAI.CubicFirstMoment.cubicSymbol_neg line 59

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:294 (same declaration text).

  6. lemma OAI.CubicFirstMoment.cubicSymbol_conjugate line 70

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:305 (same declaration text).

  7. lemma OAI.CubicFirstMoment.reciprocity_of_prime_divisor_relation line 83

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:318 (same declaration text).

  8. lemma OAI.CubicFirstMoment.same_char_primary_primes line 99

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:334 (same declaration text).

  9. lemma OAI.CubicFirstMoment.cubic_reciprocity_conjugate line 124

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:361 (same declaration text).

  10. theorem OAI.CubicFirstMoment.cubic_reciprocity_prime line 181

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:419 (same declaration text).

  11. theorem OAI.CubicFirstMoment.cubic_reciprocity line 189

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:429 (same declaration text).

  12. theorem OAI.CubicFirstMoment.gauss_twisted_mul line 215

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:457 (same declaration text).

  13. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_sq_eq_star line 219

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:461 (same declaration text).

  14. lemma OAI.CubicFirstMoment.cubicSymbol_sq_eq_star line 228

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:470 (same declaration text).

  15. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_eq_zero_of_dvd line 238

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:480 (same declaration text).

  16. lemma OAI.CubicFirstMoment.cubicSymbol_eq_zero_of_not_isCoprime line 245

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:487 (same declaration text).

  17. theorem OAI.CubicFirstMoment.gauss_mul line 261

    Also declared: OAI/NumberTheory/CubicGauss/Reciprocity.lean:504 (same declaration text).