Commit 2024-04-30 09:33 35a84817

View on Github →

chore(NumberField/Units): split into two files (#12509) This PR splits the file NumberField/Units.lean into two files placed into a new folder NumberField/Units:

Units/Basic.lean contains the basic definitions and results about the unit group and its torsion subgroup,
Units/DirichletTheorem.lean contains the proof of Dirichlet unit theorem and results about the structure of the unit group and its rank.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/Units/Basic.lean

added theorem NumberField.Units.coe_injective

added theorem NumberField.Units.coe_mul

added theorem NumberField.Units.coe_ne_zero

added theorem NumberField.Units.coe_neg_one

added theorem NumberField.Units.coe_one

added theorem NumberField.Units.coe_pow

added theorem NumberField.Units.coe_zpow

added theorem NumberField.Units.mem_torsion

added theorem NumberField.Units.rootsOfUnity_eq_one

added theorem NumberField.Units.rootsOfUnity_eq_torsion

added def NumberField.Units.torsion

added def NumberField.Units.torsionOrder

added theorem NumberField.isUnit_iff_norm

added theorem Rat.RingOfIntegers.isUnit_iff

Renamed Mathlib/NumberTheory/NumberField/Units.lean to Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

deleted def NumberField.Units.basisModTorsion

deleted theorem NumberField.Units.coe_injective

deleted theorem NumberField.Units.coe_mul

deleted theorem NumberField.Units.coe_ne_zero

deleted theorem NumberField.Units.coe_neg_one

deleted theorem NumberField.Units.coe_one

deleted theorem NumberField.Units.coe_pow

deleted theorem NumberField.Units.coe_zpow

added def NumberField.Units.dirichletUnitTheorem.basisModTorsion

added theorem NumberField.Units.dirichletUnitTheorem.exist_unique_eq_mul_prod

added theorem NumberField.Units.dirichletUnitTheorem.fun_eq_repr

added def NumberField.Units.dirichletUnitTheorem.fundSystem

added def NumberField.Units.dirichletUnitTheorem.rank

added theorem NumberField.Units.dirichletUnitTheorem.rank_modTorsion

added def NumberField.Units.dirichletUnitTheorem.unitLatticeEquiv

added theorem NumberField.Units.dirichletUnitTheorem.unitLattice_rank

deleted theorem NumberField.Units.exist_unique_eq_mul_prod

deleted theorem NumberField.Units.fun_eq_repr

deleted def NumberField.Units.fundSystem

deleted theorem NumberField.Units.mem_torsion

deleted def NumberField.Units.rank

deleted theorem NumberField.Units.rank_modTorsion

deleted theorem NumberField.Units.rootsOfUnity_eq_one

deleted theorem NumberField.Units.rootsOfUnity_eq_torsion

deleted def NumberField.Units.torsion

deleted def NumberField.Units.torsionOrder

deleted def NumberField.Units.unitLatticeEquiv

deleted theorem NumberField.Units.unitLattice_rank

deleted theorem NumberField.isUnit_iff_norm

deleted theorem Rat.RingOfIntegers.isUnit_iff