Commit 2026-03-06 23:17 1b2df6c9

View on Github →

feat: some lemmas about finite index subgroups/submodules (#36227) This adds some results on the (quotient by the) image of the nth power / multiplication-by-n map and related material on the (relative) index of a subgroup / submodule. These are helpful for proving the Northcott property of heights on number fields.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Map.lean

added theorem Subgroup.subgroupOf_mono

Modified Mathlib/GroupTheory/FiniteAbelian/Basic.lean

added theorem Subgroup.finiteIndex_range_powMonoidHom_of_fg

added theorem Subgroup.isFiniteRelIndex_map_powMonoidHom_of_fg

added theorem Submodule.fg_toAddSubgroup

added theorem Submodule.isFiniteRelIndex_of_map_linearMapMulLeft_le

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.isFiniteRelIndex_iff_finiteIndex

added theorem Subgroup.isFiniteRelIndex_iff_relIndex_ne_zero

added theorem Subgroup.isFiniteRelIndex_of_le

modified theorem Subgroup.not_finiteIndex_iff

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem Subgroup.pow_relIndex_mem

Modified Mathlib/GroupTheory/Torsion.lean

added theorem CommGroup.isTorsion_quotient_range_powMonoidHom