specialUnitaryGroup_le_unitaryGroup

Mathlib.LinearAlgebra.UnitaryGroup

URI: https://scilib.ai/kg/mathlib#Matrix.specialUnitaryGroup_le_unitaryGroup

English

The special unitary group is contained in the unitary group.

Русский

Специализированная унитарная группа содержится в унитарной группе.

LaTeX

$$specialUnitaryGroup n α ≤ unitaryGroup n α$$

Lean4

theorem specialUnitaryGroup_le_unitaryGroup : specialUnitaryGroup n α ≤ unitaryGroup n α :=
  inf_le_left

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

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

Разделы

Аффилиация

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