OAI/NumberTheory/PrimePackets/RayDescent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.EvenRayCharacter.underlyingIdeal_integralUnit line 15
  2. lemma OAI.PrimeDegreePackets.EvenRayCharacter.coprime_inverse_product line 23
  3. theorem OAI.PrimeDegreePackets.EvenRayCharacter.idealHom_eq_of_coprime_class line 55
  4. def OAI.PrimeDegreePackets.EvenRayCharacter.classValue line 78
  5. lemma OAI.PrimeDegreePackets.EvenRayCharacter.idealHom_eq_classValue line 81
  6. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classValue_one line 89
  7. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classValue_mul line 96
  8. def OAI.PrimeDegreePackets.EvenRayCharacter.classCharacter line 112
  9. lemma OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient_of_residue_one line 117
  10. def OAI.PrimeDegreePackets.EvenRayCharacter.classUnitCharacter line 127
  11. def OAI.PrimeDegreePackets.classRayCharacter line 138
  12. lemma OAI.PrimeDegreePackets.EvenRayCharacter.coprime_modulus_one line 163
  13. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classRay_coefficient line 169
  14. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classRay_dirichlet line 175
  15. lemma OAI.PrimeDegreePackets.EvenRayCharacter.coprime_idealOverPrime_iff line 182