coe_mk

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

English

The underlying matrix of an element of SL equals the representative matrix.

Русский

Опорная матрица элемента SL совпадает с представленной матрицей.

LaTeX

$$$ \operatorname{val}(\langle A, h\rangle) = A $$$

Lean4

theorem coe_mk (A : Matrix n n R) (h : det A = 1) : ↑(⟨A, h⟩ : SpecialLinearGroup n R) = A :=
  rfl

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

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

Разделы

Аффилиация

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