Erdős Problem 274

References: erdosproblems.com/274 Wikipedia

theorem Erdos274.erdos_274 (G : Type u_1) [Group G] (hG : 1 < ENat.card G) : (∃ (P : Partition ⊤), 1 < P.parts.ncard ∧ (∀ A ∈ P.parts, ∃ (s : G) (H : Subgroup G), s • ↑H = ↑A) ∧ P.parts.Pairwise fun (A B : Subgroup G) => Cardinal.mk ↥A ≠ Cardinal.mk ↥B) ↔ sorry

If G is a group then can there exist an exact covering of G by more than one cosets of different sizes? (i.e. each element is contained in exactly one of the cosets.)

theorem Erdos274.erdos_274.variants.abelian (G : Type u_1) [Fintype G] [CommGroup G] (hG : 1 < Fintype.card G) (P : Partition ⊤) (hP : 1 < P.parts.ncard) (h : ∀ A ∈ P.parts, ∃ (s : G) (H : Subgroup G), s • ↑H = ↑A) : ∃ A ∈ P.parts, ∃ B ∈ P.parts, A ≠ B ∧ A.index = B.index

If G is a finite abelian group then there cannot exist an exact covering of G by more than one cosets of different sizes? (i.e. each element is contained in exactly one of the cosets.)

theorem Erdos274.herzog_schonheim (G : Type u_1) [Group G] (hG : 1 < ENat.card G) (P : Partition ⊤) : 1 < P.parts.ncard → (∀ B ∈ P.parts, ∃ (s : G) (H : Subgroup G), s • ↑H = ↑B) → ∃ A ∈ P.parts, ∃ B ∈ P.parts, A ≠ B ∧ A.index = B.index

Let $G$ be a group, and let $A = \{a_1G_1, \dots, a_kG_k\}$ be a finite system of left cosets of subgroups $G_1, \dots, G_k$ of $G$.

Herzog and Schönheim conjectured that if $A$ forms a partition of $G$ with $k > 1$, then the indices $[G:G_1], \dots, [G:G_k]$ cannot be distinct.