Erdős problem 274

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/274.lean

Formal Conjectures

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

Reported activity

Reported by these sources. Not reviewed here.

Solved as stated, hidden constraints
GPT-Erdős
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry