Erdős problem 274 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

274.lean

Retained formal statement3 of 3

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.

FormalConjectures/ErdosProblems/274.leanErdos274.herzog_schonheim5 linesExact file

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

OpenStatement only, no proof

Sources

Search problems.science