OAI/NumberTheory/CubicGram/PrimaryNormalization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Unique primary associates and canonical prime factorization.

  1. lemma OAI.CubicFirstMoment.normNat_of_isUnit line 16

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

  2. lemma OAI.CubicFirstMoment.norm_of_isUnit line 19

    Also declared: OAI/NumberTheory/CubicGauss/HeckeIdeals.lean:19 (same declaration text).

  3. lemma OAI.CubicFirstMoment.primary_iff_residue_one line 22
  4. lemma OAI.CubicFirstMoment.primary_mul line 28
  5. lemma OAI.CubicFirstMoment.primary_unit_eq_one line 32
  6. lemma OAI.CubicFirstMoment.primary_associated_eq line 59
  7. lemma OAI.CubicFirstMoment.residue_three_eq_zero line 68
  8. lemma OAI.CubicFirstMoment.residue_ofCoords_mod_three line 71
  9. lemma OAI.CubicFirstMoment.residue_three_nontrivial line 85
  10. lemma OAI.CubicFirstMoment.omegaE_isUnit line 92
  11. lemma OAI.CubicFirstMoment.unit_lift_mod_three line 96
  12. lemma OAI.CubicFirstMoment.unit_residue_of_dvd_primary line 148
  13. def OAI.CubicFirstMoment.primaryNormalize line 154
  14. lemma OAI.CubicFirstMoment.primaryNormalize_associated line 159
  15. lemma OAI.CubicFirstMoment.primaryNormalize_primary line 165
  16. lemma OAI.CubicFirstMoment.primaryNormalize_eq_self line 170
  17. lemma OAI.CubicFirstMoment.exists_unique_primary_associate line 175
  18. lemma OAI.CubicFirstMoment.normNat_primaryNormalize line 183
  19. lemma OAI.CubicFirstMoment.prime_primaryNormalize line 186
  20. lemma OAI.CubicFirstMoment.primaryNormalize_injOn_primeFactors line 189
  21. def OAI.CubicFirstMoment.primaryPrimeFactors line 196
  22. lemma OAI.CubicFirstMoment.primaryPrimeFactor_spec line 199
  23. lemma OAI.CubicFirstMoment.primary_finset_prod line 208
  24. lemma OAI.CubicFirstMoment.primaryPrimeFactors_prod line 218
  25. lemma OAI.CubicFirstMoment.primaryPrimeFactors_card line 230
  26. lemma OAI.CubicFirstMoment.primaryPrimeFactors_norm_prod line 234