coe_mul_star_self

Mathlib.Algebra.Star.Unitary

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

English

Let R be a monoid equipped with an involutive star operation. If U is a unitary element of R, then U · star(U) = 1.

Русский

Пусть R — моноид с инволютивной операцией звезда. Если U — унитарный элемент R, то U · U^{*} = 1.

LaTeX

$$$ U \in \mathrm{Unitary}(R) \Rightarrow U \star U = 1 $$$

Lean4

theorem coe_mul_star_self (U : unitary R) : (U : R) * star U = 1 :=
  mul_star_self_of_mem U.prop

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

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

Разделы

Аффилиация

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