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

Sources

Search problems.science