instInvSubtypeMemSubmonoidSpecialUnitaryGroup

Mathlib.LinearAlgebra.UnitaryGroup

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

English

In the special unitary group, the inverse of an element is given by its star (conjugate transpose).

Русский

В группе специальной унитарной обратный к элементу задаётся звёздой (сопряжённой транспозе).

LaTeX

$$$\\forall A \\in \\mathrm{specialUnitaryGroup}(n,\\alpha),\\quad A^{-1} = \\star A$$$

Lean4

instance : Inv (specialUnitaryGroup n α) where inv := star

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

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

Разделы

Аффилиация

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