FormalConjectures/Kourovka/8_8.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 2 contain sorry, 0 declared as axioms

Conjecture 8.8

by R. I. Grigorchuk

Both parts of the problem are due to D. V. Anosov.

Reference: The Kourovka Notebook

Imports (1)
  1. theorem Kourovka.«8.8».kourovka_8_8a Does there exist a non-cyclic finitely-generated group $G$ containing an element $a$ such that every element of $G$ is conjugate to a power of $a$? sorry line 44 source

    Source documentation

    Does there exist a non-cyclic finitely-generated group $G$ containing an element $a$ such that every element of $G$ is conjugate to a power of $a$?

    Here a power of $a$ means $a^n$ for some $n \in \mathbb{Z}$.

    Answered affirmatively by V. S. Guba, Math. USSR-Izv. 29 (1986), 233–277.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Group, And, Not, IsCyclic, Group.FG, Int, IsConj, HPow.hPow

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

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem kourovka_8_8a : answer(True) ↔
    ∃ (G : Type) (_ : Group G), ¬ IsCyclic G ∧ Group.FG G ∧
      ∃ a : G, ∀ g : G, ∃ n : ℤ, IsConj g (a ^ n) := by
…
  2. theorem Kourovka.«8.8».kourovka_8_8b Does there exist a non-cyclic finitely presented group $G$ which contains an element $a$ such that each element of $G$ is conjugate to some power of $a$? sorry line 56 source

    Source documentation

    Does there exist a non-cyclic finitely presented group $G$ which contains an element $a$ such that each element of $G$ is conjugate to some power of $a$?

    Here a power of $a$ means $a^n$ for some $n \in \mathbb{Z}$.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Group, And, Not, IsCyclic, Group.IsFinitelyPresented, Int, IsConj, HPow.hPow

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

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem kourovka_8_8b : answer(sorry) ↔
    ∃ (G : Type) (_ : Group G), ¬ IsCyclic G ∧ Group.IsFinitelyPresented G ∧
      ∃ a : G, ∀ g : G, ∃ n : ℤ, IsConj g (a ^ n) := by
…