A counterexample to the unit conjecture for group rings

Problem statement

Notes: Unavailable.

Source: G. Gardam, `A counterexample to the unit conjecture for group rings`, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-3-UnitConjecture.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_A : (∀ g : UnitConjecture.P, ∀ n ≠ 0, g ^ n = 1 → g = 1) ∧ IsUnit UnitConjecture.u ∧ ¬ ∃ g : UnitConjecture.P, UnitConjecture.u = g := by⊢ (∀ (g : P) (n : ℕ), n ≠ 0 → g ^ n = 1 → g = 1) ∧ IsUnit u ∧ ¬∃ g, u = (MonoidAlgebra.of (ZMod 2) P) g
  sorryAll goals completed! 🐙