star_eq_inv — Mathlib

English

The specialUnitaryGroup n α forms a group under matrix multiplication, with the inverse given by the star operation.

Русский

Группа специальной унитарной матриц размерности n образована по умножению матриц, обратное равно звезде.

LaTeX

$$$(\\mathrm{specialUnitaryGroup}(n,\\alpha), \\cdot, {}^{-1}) \\text{ is a group with } a^{-1}=a^{*}$ for all $a$.$$

Lean4

theorem star_eq_inv (A : specialUnitaryGroup n α) : star A = A⁻¹ :=
  rfl

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