isConj_iff — Mathlib

English

In a group, IsConj a b iff there exists c with c a c^{-1} = b.

Русский

В группе IsConj a b эквивалентно существованию c such that c a c^{-1} = b.

LaTeX

$$$IsConj(a,b) \\iff \\exists c : \\mathsf{Group}, c a c^{-1} = b$$$

Lean4

@[simp]
theorem isConj_iff {a b : α} : IsConj a b ↔ ∃ c : α, c * a * c⁻¹ = b :=
  ⟨fun ⟨c, hc⟩ => ⟨c, mul_inv_eq_iff_eq_mul.2 hc⟩, fun ⟨c, hc⟩ =>
    ⟨⟨c, c⁻¹, mul_inv_cancel c, inv_mul_cancel c⟩, mul_inv_eq_iff_eq_mul.1 hc⟩⟩

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