isParabolic_conj_iff — Mathlib

English

In GL2, conjugating a parabolic element by any invertible matrix preserves parabolicity: IsParabolic(g h g^{-1}) iff IsParabolic h.

Русский

В GL2 конъюгация параболического элемента произвольной обратимой матрицей сохраняет параболичность: IsParabolic(g h g^{-1}) эквивално IsParabolic(h).

LaTeX

$$$IsParabolic\bigl(g h g^{-1}\bigr) \iff IsParabolic(h)$$$

Lean4

@[simp]
theorem isParabolic_conj_iff [Nontrivial R] (g h : GL (Fin 2) R) : IsParabolic (g * h * g⁻¹) ↔ IsParabolic h := by
  simp [IsParabolic]

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