Commit 2025-03-18 06:37 96f29be0

View on Github →

feat(NumberTheory/NumberField): torsion units in number fields of odd degree (#22297) Add basic lemmas about number fields of odd degree. In particular, prove that the order of the torsion subgroup is equal to two.

Estimated changes

Modified Mathlib/Algebra/CharP/Two.lean

added theorem CharP.orderOf_eq_two_iff

Modified Mathlib/Dynamics/PeriodicPts/Lemmas.lean

added theorem Function.minimalPeriod_eq_prime_iff

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem orderOf_eq_prime_iff

Modified Mathlib/GroupTheory/Torsion.lean

added theorem neg_one_mem_torsion

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank

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

added theorem NumberField.Units.torsionOrder_eq_two_of_odd_finrank

added theorem NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank