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 statement2 of 3

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

FormalConjectures/ErdosProblems/274.leanErdos274.erdos_274.variants.abelian4 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science