OAI/NumberTheory/PrimePackets/PrincipalUnits.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.integralIdealFractionalUnit_top line 145
  2. def OAI.PrimeDegreePackets.principalUnitFiber line 150
  3. def OAI.PrimeDegreePackets.principalUnitElement line 154
  4. lemma OAI.PrimeDegreePackets.principalUnitElement_class line 158
  5. lemma OAI.PrimeDegreePackets.idealResidueCoefficient_principalUnit line 164
  6. def OAI.PrimeDegreePackets.principalResidueDirichlet line 177
  7. theorem OAI.PrimeDegreePackets.principalResidueDirichlet_tendsto line 185
  8. theorem OAI.PrimeDegreePackets.residuePrincipalContinued_ne_zero line 233
  9. theorem OAI.PrimeDegreePackets.residuePrincipal_finite_nonnegative_order line 250
  10. theorem OAI.PrimeDegreePackets.exists_simultaneous_ideal_generator line 281
  11. lemma OAI.PrimeDegreePackets.exists_nonzero_simultaneous_ideal_generator line 315
  12. theorem OAI.PrimeDegreePackets.exists_coprime_ideal_product line 331
  13. theorem OAI.PrimeDegreePackets.exists_coprime_class_representative line 362
  14. def OAI.PrimeDegreePackets.coprimeClassRepresentative line 387
  15. lemma OAI.PrimeDegreePackets.coprimeClassRepresentative_spec line 391
  16. theorem OAI.PrimeDegreePackets.exists_residueClassContinued line 399