toGL_one

Mathlib.LinearAlgebra.UnitaryGroup

URI: https://scilib.ai/kg/mathlib#Matrix.UnitaryGroup.toGL_one

English

The map toGL is a homomorphism: toGL(A B) = toGL(A) toGL(B).

Русский

Отображение toGL является гомоморфизмом: toGL(A B) = toGL(A) toGL(B).

LaTeX

$$toGL(A B) = toGL(A) · toGL(B)$$

Lean4

@[simp]
theorem toGL_one : toGL (1 : unitaryGroup n α) = 1 :=
  Units.ext <| by
    simp only [coe_toGL, toLin'_one]
    rfl

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

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

Разделы

Аффилиация

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