Commit 2025-04-18 17:47 3acfa399

feat: typeclass for subgroups of finite relative index (#23596) This is useful to state the following: https://github.com/ImperialCollegeLondon/FLT/blob/c51f2573c22ded973f354f56f598507b0f349f51/FLT/Mathlib/MeasureTheory/Group/Action.lean#L57-L59 namely that the Haar measure of a subgroup H of finite index inside a subgroup K is the Haar measure of K divided by the index. A possible alternative would be to have some ENat-valued index. From FLT