_example — Mathlib

English

The unitaryGroup n α is the submonoid of n×n matrices over α consisting of those A for which the star-transpose is the inverse.

Русский

Группа Юнитарных матриц n×n над α — это подмономоида, состоящий из матриц A, для которых A^* A = I = A A^*.

LaTeX

$$$ \mathrm{unitaryGroup}_{n}(\alpha) = \{ A \in M_{n}(\alpha) : A^{*} A = I = A A^{*} \}. $$$

Lean4

example : Group (unitaryGroup n α) :=
  inferInstance

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