star_eq_inv

Mathlib.Algebra.Star.Unitary

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

English

For a unitary element U, star(U) = U^{-1}.

Русский

Для унитарного элемента U звезда(U) равна обратному U^{-1}.

LaTeX

$$$ \star U = U^{-1} $$$

Lean4

theorem star_eq_inv (U : unitary R) : star U = U⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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