Theorem Subgroup.Commensurable.commensurator_mem_iff

Modification history

2025-09-25 05:05
Mathlib/GroupTheory/Commensurable.lean
feat(GroupTheory/Commensurable): additivize (#29707) …
Added Subgroup.Commensurable.commensurator_mem_iffView on Github →