erdos_274.variants.abelian

Specification

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

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem erdos_274.variants.abelian {G : Type*} [Fintype G] [CommGroup G]
    (hG : 1 < Fintype.card G) {ι : Type*} [Fintype ι] (P : Group.ExactCovering G ι)
    (hι : 1 < Fintype.card ι) :
    ∃ i j, i ≠ j ∧ #(P.parts i) = #(P.parts j)

ID: ErdosProblems__274__erdos_274.variants.abelian

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.