mul_star_self_of_mem

Mathlib.Algebra.Star.Unitary

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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