coe_toGL

Mathlib.LinearAlgebra.UnitaryGroup

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

English

The underlying matrix of toGL(A) equals toLin'(A).

Русский

Базовая матрица toGL(A) совпадает с toLin'(A).

LaTeX

$$toGL(A).val = toLin'(A)$$

Lean4

theorem coe_toGL (A : unitaryGroup n α) : (toGL A).1 = toLin' A :=
  rfl

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

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

Разделы

Аффилиация

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