star_mul_self_of_mem

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.star_mul_self_of_mem

English

If U is unitary, then star U · U = 1.

Русский

Если U унитарен, то star U · U = 1.

LaTeX

$$$ star U \cdot U = 1 $$$

Lean4

@[simp]
theorem star_mul_self_of_mem {U : R} (hU : U ∈ unitary R) : star U * U = 1 :=
  hU.1

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

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

Разделы

Аффилиация

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