isConj_iff₀ — Mathlib

English

IsConj a b holds iff there exists c ≠ 0 with c a c^{-1} = b.

Русский

IsConj a b эквивалентно существованию c ≠ 0 такого, что c a c^{-1} = b.

LaTeX

$$$IsConj(a,b) \iff \exists c \neq 0,\ c a c^{-1} = b$$$

Lean4

@[simp]
theorem isConj_iff₀ : IsConj a b ↔ ∃ c : α, c ≠ 0 ∧ c * a * c⁻¹ = b :=
  by
  rw [IsConj, Units.exists_iff_ne_zero (p := (SemiconjBy · a b))]
  congr! 2 with c
  exact and_congr_right (mul_inv_eq_iff_eq_mul₀ · |>.symm)

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