toGL_mul

Mathlib.LinearAlgebra.UnitaryGroup

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

English

Another statement that toGL preserves multiplication: toGL(A B) equals toGL(A) times toGL(B).

Русский

Еще одно утверждение: toGL сохраняет умножение: toGL(A B) = toGL(A) toGL(B).

LaTeX

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

Lean4

@[simp]
theorem toGL_mul (A B : unitaryGroup n α) : toGL (A * B) = toGL A * toGL B :=
  Units.ext <| by
    simp only [coe_toGL, toLin'_mul]
    rfl

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

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

Разделы

Аффилиация

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