isParabolic_conj_iff' — Mathlib

English

The same conjugation-invariance for parabolicity holds with alternative conjugation ordering: IsParabolic(g^{-1} h g) iff IsParabolic h.

Русский

Тождественная нормализация параболичности при сопряжении с другой постановкой: IsParabolic(g^{-1} h g) эквивалентно IsParabolic h.

LaTeX

$$$IsParabolic\bigl(g^{-1} h g\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]

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