Commit 2024-08-18 22:27 5dccde47
View on Github →feat(GroupTheory/Index): index_toAddSubgroup (#15946)
Add simp lemmas relating indexes of additive and multiplicative subgroups, as converted with Subgroup.toAddSubgroup and AddSubgroup.toSubgroup, all proved with rfl.
From AperiodicMonotilesLean.