Commit 2024-10-21 09:28 8a8d36d5

feat(GroupTheory/Index): index of product of subgroups (#17878) Add two lemmas about the index of a product (pairwise or indexed) of subgroups.

@[to_additive]
lemma index_prod (H : Subgroup G) (K : Subgroup G') : (H.prod K).index = H.index * K.index := by

@[to_additive]
lemma index_pi {ι : Type*} [Fintype ι] (H : ι → Subgroup G) :
    (Subgroup.pi Set.univ H).index = ∏ i, (H i).index := by

From AperiodicMonotilesLean.