Commit 2025-09-01 13:46 f47dc948

View on Github →

feat(NumberField/Units): compute index of unit subgroups using regulators (#26075)

depends on: #25730

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.not_finiteIndex_iff

added theorem Subgroup.relindex_map_map

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

added theorem NumberField.Units.dirichletUnitTheorem.closure_fundSystem_sup_torsion_eq_top

added theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_ker

added theorem NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion

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

added theorem NumberField.Units.regOfFamily_div_regOfFamily

added theorem NumberField.Units.regOfFamily_div_regulator

added theorem NumberField.Units.span_basisOfIsMaxRank