mem_commutatorSet_of_isConj_sq — Mathlib

English

If g is conjugate to g^2, then g lies in the commutatorSet G.

Русский

Если g конъюгировано к g^2, то g принадлежит commutatorSet(G).

LaTeX

$$$ \\text{IsConj}(g,g^2) \\Rightarrow g \\in commutatorSet(G) $$$

Lean4

/-- If g is conjugate to g ^ 2, then g is a commutator -/
theorem mem_commutatorSet_of_isConj_sq {g : G} (hg : IsConj g (g ^ 2)) : g ∈ commutatorSet G :=
  by
  obtain ⟨h, hg⟩ := hg
  use h, g
  rw [commutatorElement_def, hg]
  simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]

Похожие утверждения