Commit 2026-06-07 01:53 93a6021d

View on Github →

feat: add NumberField.Units.finrank_eq (#40239) From flt-regular.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Torsion/Basic.lean

added theorem finrank_quotient_eq_of_le_torsion

added theorem finrank_quotient_torsion_eq

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

added theorem NumberField.Units.dirichletUnitTheorem.finrank_eq

added theorem NumberField.Units.dirichletUnitTheorem.finrank_modTorsion

deleted theorem NumberField.Units.dirichletUnitTheorem.rank_modTorsion