FormalConjectures/ErdosProblems/274.lean

GitHub source file

4 declarations, 3 contain sorry, 0 declared as axioms

1. structure Erdos274.Group.ExactCovering Documented declaration: ExactCovering line 48 source

   Source documentation

   An exact covering of a group G is a finite collection of subgroups {H_1, ..., H_k} and representative {g_1, ..., g_k} such that the cosets g_iH_i are pairwise disjoint and their union covers G.

   Note that this differs from Partition (α := Subgroup G) because the covering condition there invokes Subgroup.sup which is subgroup generation and thus stronger than union. This definition is easier to use in this context than the alternative Partition (α := Set G), which lacks subgroup definitions such as Subgroup.index.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Group, Fintype

   structure Group.ExactCovering (G : Type*) [Group G] (ι : Type*) [Fintype ι] where
   …

2. theorem Erdos274.erdos_274 If $G$ is a group, can there exist an exact covering of $G$ by more than one coset of different sizes? sorry line 63 source

   Source documentation

   If $G$ is a group, can there exist an exact covering of $G$ by more than one coset of different sizes? (i.e. each element is contained in exactly one of the cosets.)

   The conjectured answer is no: in every such exact covering, two of the subgroups have the same cardinality.

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Group, And, LT.lt, ENat, OfNat.ofNat, ENat.card, Fintype, Erdos274.Group.ExactCovering, Nat, Fintype.card, Ne, Cardinal, Cardinal.mk, Subtype, Membership.mem, Subgroup, Erdos274.Group.ExactCovering.parts

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   16 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_274 : answer(sorry) ↔ ∃ (G : Type*) (_ : Group G),
       1 < ENat.card G ∧ ∃ (ι : Type*) (_ : Fintype ι) (P : Group.ExactCovering G ι),
       1 < Fintype.card ι ∧ ∀ i j, i ≠ j → #(P.parts i) ≠ #(P.parts j) := by
   …

   Mentions: Erdos274.Group.ExactCovering

3. theorem Erdos274.erdos_274.variants.abelian sorry line 75 source

   depends on sorry what this means

   Statement uses: Fintype, CommGroup, LT.lt, Nat, OfNat.ofNat, Fintype.card, Erdos274.Group.ExactCovering, Exists, And, Ne, Eq, Cardinal, Cardinal.mk, Subtype, Membership.mem, Subgroup, Erdos274.Group.ExactCovering.parts

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

4. theorem 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$ sorry line 89 source

   Source documentation

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

   Herzog and Schönheim conjectured that if $A$ forms a partition of $G$ with $k > 1$, then the indices $[G:G_1], \dots, [G:G_k]$ cannot be distinct.

   depends on sorry what this means

   Statement uses: Group, LT.lt, ENat, OfNat.ofNat, ENat.card, Fintype, Nat, Fintype.card, Erdos274.Group.ExactCovering, Exists, And, Ne, Eq, Subgroup.index, Erdos274.Group.ExactCovering.parts

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   12 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem herzog_schonheim {G : Type*} [Group G] (hG : 1 < ENat.card G) {ι : Type*} [Fintype ι]
       (hι : 1 < Fintype.card ι) (P : Group.ExactCovering G ι) :
       ∃ i j, i ≠ j ∧ (P.parts i).index = (P.parts j).index := by
   …

   Mentions: Erdos274.Group.ExactCovering