isParabolic_conj'_iff

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

URI: https://scilib.ai/kg/mathlib#Matrix.isParabolic_conj'_iff

English

For g in GL(2), (g^{-1} m g) is parabolic iff m is parabolic.

Русский

Для g ∈ GL(2), (g^{-1} m g) параболична тогда и только тогда, когда m параболична.

LaTeX

$$$ (g^{-1} m g).IsParabolic \iff m.IsParabolic.$$$

Lean4

@[simp]
theorem isParabolic_conj'_iff : (g.val⁻¹ * m * g.val).IsParabolic ↔ m.IsParabolic := by
  simpa using isParabolic_conj_iff g⁻¹

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru