1) V1 If a nontrivial group is partitioned into more than one left coset from a finite family of subgroups, then two different subgroups in the partition have the same index.
open, filed Tue Aug 25 2026 04:06:35 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Formal written first and checked term by term. A left coset is reps i • parts i; PairwiseDisjoint plus union equal to univ means exact partition; Fintype gives finitely many cosets; Subgroup.index expresses [G:H]; the conclusion repeats an index at distinct labels. Subgroup cosets are automatically nonempty, so the source formalization's nonempty field is redundant. Search asymmetry is the kernel-checked finite-index reduction: exactness plus Mathlib's Neumann theorem forces every part, not merely one part, to have finite index.
Scope. Universal over groups G, finite index types ι, subgroup families and representatives. The cosets are pairwise disjoint and cover G; when |ι| > 1, two distinct parts must have equal subgroup index.