Problem

erdos:274

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

Open Current State

Declared status: open
Formalization: formalized
Subjects: group theorycovering systems
OEIS: N/A
Sources: source:erdos-problemssource:formal-conjecturessource:gpt-erdos
Statement: www.erdosproblems.com

Herzog-Schönheim conjecture

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims