isElliptic_conj_iff

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

URI: https://scilib.ai/kg/mathlib#Matrix.isElliptic_conj_iff

English

Conjugation preserves ellipticity: IsElliptic(g m g^{-1}) iff IsElliptic(m).

Русский

Конъюгация сохраняет эллиптику: IsElliptic(g m g^{-1}) ⇔ IsElliptic(m).

LaTeX

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

Lean4

theorem isElliptic_conj_iff : (g.val * m * g.val⁻¹).IsElliptic ↔ m.IsElliptic := by simp [IsElliptic]

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

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

Разделы

Аффилиация

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