Commit 2026-08-18 11:28 6f01f5d2

View on Github →

refactor(GroupTheory/Commensurable): add and generalize API (#41030) This PR makes the following changes to GroupTheory/Commensurable.lean:

  • Use IsFiniteRelIndex instead of relIndex ≠ 0 to allow use of IsFiniteRelIndex API.
  • Add API lemmas for bot, top, inf, map, comap, and smul.
  • Deprecate the existing conjugation API lemmas as superseded by the new smul API lemmas.
  • Define commensurator directly via MulAut.conj rather than going through ConjAct.
  • Deprecate the auxiliary commensurator'.

Estimated changes

modified theorem Subgroup.Commensurable.comm
modified theorem Subgroup.Commensurable.eq
modified theorem Subgroup.Commensurable.symm