instPowNat

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

URI: https://scilib.ai/kg/mathlib#Matrix.SpecialLinearGroup.instPowNat

English

The nth power of a matrix in SL(n,R) also lies in SL(n,R); determinant remains 1.

Русский

Степень n матрицы из SL(n,R) тоже принадлежит SL(n,R); детерминант сохраняется равным 1.

LaTeX

$$Pow (SpecialLinearGroup n R) Nat$$

Lean4

instance : Pow (SpecialLinearGroup n R) ℕ where pow x n := ⟨x ^ n, (det_pow _ _).trans <| x.prop.symm ▸ one_pow _⟩

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

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

Разделы

Аффилиация

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