isElliptic_conj'_iff — Mathlib

English

For any g in GL2(R) and any 2×2 matrix m over a commutative ring with a preorder, the elliptic property is preserved under conjugation: (g^{-1} m g) is elliptic if and only if m is elliptic.

Русский

Для любой g ∈ GL_2(R) и любой матрицы m размером 2×2 над коммутативным кольцом с предпорядком свойство эллиптическости сохраняется при сопряжении: g^{-1} m g эллиптично тогда и только тогда, когда m эллиптично.

LaTeX

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

Lean4

theorem isElliptic_conj'_iff : (g.val⁻¹ * m * g.val).IsElliptic ↔ m.IsElliptic := by simpa using isElliptic_conj_iff g⁻¹

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