isHyperbolic_conj'_iff

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

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

English

An equivalent statement: (g.m.g^{-1}) IsHyperbolic iff m IsHyperbolic, or with inverse placement as in the theorems.

Русский

Эквивалентно: (g m g^{-1}) IsHyperbolic ⇔ m IsHyperbolic, с учётом порядка г.

LaTeX

$$(g.m.g^{-1}).IsHyperbolic ⇔ m.IsHyperbolic$$

Lean4

theorem isHyperbolic_conj'_iff : (g.val⁻¹ * m * g.val).IsHyperbolic ↔ m.IsHyperbolic := by
  simpa using isHyperbolic_conj_iff g⁻¹

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

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

Разделы

Аффилиация

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