OAI/NumberTheory/CubicGram/ReciprocityKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite-field Frobenius relations and distinct-character reciprocity.

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

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

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

    Distinct definitions of this name: OAI/NumberTheory/CubicGauss/Reciprocity.lean:38 (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 105

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

  4. lemma OAI.CubicFirstMoment.cubeRoot_reduce_inj line 109

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

  5. lemma OAI.CubicFirstMoment.cubicResidueCharE_cube line 118

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

  6. lemma OAI.CubicFirstMoment.cubicResidueCharE_neg_one line 128

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

  7. lemma OAI.CubicFirstMoment.cubicResidueCharE_value_cube line 136

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

  8. lemma OAI.CubicFirstMoment.cubicResidueCharE_ringHomComp_ne_one line 145

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

  9. lemma OAI.CubicFirstMoment.primeJacobi_eq_sumE line 161

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

  10. lemma OAI.CubicFirstMoment.normNat_cast_eq_mul_conjugate line 168

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

  11. lemma OAI.CubicFirstMoment.cubic_reciprocity_frobenius line 175

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

  12. theorem OAI.CubicFirstMoment.cubic_reciprocity_distinct_char line 234

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