star_eq_inv'

Mathlib.Algebra.Star.Unitary

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

English

The star operation on unitary elements coincides with the inverse map.

Русский

Операция звезды на унитарных элементах совпадает с отображением наобратное.

LaTeX

$$$ (star : \mathrm{unitary}(R) \to \mathrm{unitary}(R)) = (\mathrm{Inv}.inv) $$$

Lean4

theorem star_eq_inv' : (star : unitary R → unitary R) = Inv.inv :=
  rfl

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

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

Разделы

Аффилиация

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