FinitelyPresented.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The prescribed finitely presented counterexample in characteristic two.

theorem OAI.KaplanskyCounterexample.thm_main line 14
theorem OAI.KaplanskyCounterexample.finitelyPresented_counterexample line 35
Source documentation
The existential main result of the characteristic-two paper, separated from the certificates for its prescribed construction.
Distinct definitions of this name: ComparatorChallenges/KaplanskyFinitelyPresented.lean:7 (same statement text; different proof or body). Qualify references as OAI.KaplanskyCounterexample.finitelyPresented_counterexample@path.
```
theorem finitelyPresented_counterexample :
    ∃ (K : Type) (_ : Field K) (_ : Fintype K) (_ : CharP K 2),
      ∃ (G : Type) (_ : Group G) (_ : Group.IsFinitelyPresented G),
        (∃ (ℓ : ℕ) (_ : ℓ.Prime) (_ : Odd ℓ) (g : G), orderOf g = ℓ) ∧
        ∃ a_out b_out : MonoidAlgebra K G, a_out * b_out = 1 ∧ b_out * a_out ≠ 1 :=
…
```