instInvolutiveStarSubtypeMemSubmonoid

Mathlib.Algebra.Star.Unitary

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

English

The star operation on unitary elements is involutive: star(star(U)) = U for U ∈ unitary(R).

Русский

Операция звезды на унитарных элементах инволютивна: star(star(U)) = U для U ∈ unitary(R).

LaTeX

$$$ \star(\star U) = U $$$

Lean4

instance : InvolutiveStar (unitary R) :=
  ⟨by
    intro x
    ext
    rw [coe_star, coe_star, star_star]⟩

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

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

Разделы

Аффилиация

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