star_mul_self

Mathlib.LinearAlgebra.UnitaryGroup

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

English

For a unitary matrix A, its adjoint satisfies A* A = I and A A* = I; in particular, A⁻¹ = A*.

Русский

Для унитарной матрицы A выполняется A* A = I и A A* = I; следовательно, A⁻¹ = A*.

LaTeX

$$$A^{*} A = I$ (and similarly $A A^{*} = I$).$$

Lean4

theorem star_mul_self (A : unitaryGroup n α) : star A.1 * A.1 = 1 :=
  A.2.1

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

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

Разделы

Аффилиация

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