Formal target: Corpus.Erdos274.herzog_schonheim

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

Exact formal statement

∀ {G : Type u_1} [inst : Group.{u_1} G],
  LT.lt.{0} 1 (ENat.card.{u_1} G) →
    ∀ {ι : Type u_2} [inst_1 : Fintype.{u_2} ι],
      LT.lt.{0} 1 (Fintype.card.{u_2} ι) →
        ∀ (P : Corpus.Erdos274.Group.ExactCovering.{u_1, u_2} G ι),
          Exists.{u_2 + 1} fun i =>
            Exists.{u_2 + 1} fun j =>
              And (Ne.{u_2 + 1} i j)
                (Eq.{1} (Subgroup.index.{u_1} (Corpus.Erdos274.Group.ExactCovering.parts.{u_1, u_2} P i))
                  (Subgroup.index.{u_1} (Corpus.Erdos274.Group.ExactCovering.parts.{u_1, u_2} P j)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record