Commit 2023-08-02 23:55 68a37cd3

View on Github →

feat(NumberTheory.NumberField.Units): add torsion subgroup (#5748) We define the torsion subgroup of the units of a number field and prove some results about it, mostly: it is finite, cyclic and an unit is torsion iff its value is 1 at all infinite places. Some results linking to rootsOfUnity are also proved. This PR also includes a direct coercion from (𝓞 K)ˣ to K that is very convenient, although I am not sure it's done properly.

Estimated changes

Modified Mathlib/GroupTheory/Torsion.lean

added theorem CommGroup.mem_torsion

Modified Mathlib/NumberTheory/NumberField/Units.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.torsion_order

modified theorem isUnit_iff_norm