Erdős problem 274

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$ .

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

274.lean

Retained formal statement1 of 3

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

The conjectured answer is no: in every such exact covering, two of the subgroups have the same cardinality.

FormalConjectures/ErdosProblems/274.leanErdos274.erdos_2745 linesExact file

1sorry ↔2  ∀ (G : Type u_1) [inst : Group G],3    1 < ENat.card G →4      ∀ (ι : Type u_2) [inst_1 : Fintype ι] (P : Erdos274.Group.ExactCovering G ι),5        1 < Fintype.card ι → ∃ i j, i ≠ j ∧ Cardinal.mk ↥(P.parts i) = Cardinal.mk ↥(P.parts j)

OpenStatement only, no proof