instStarSubtypeMemSubmonoid

Mathlib.Algebra.Star.Unitary

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

English

There is a Star structure on the subtype consisting of unitary elements, induced by the ambient star operation.

Русский

Существуют звездные операции на подтипе узун Unitarty, порожденные внешней звездной операцией.

LaTeX

$$$\text{Star} (\mathrm{unitary}(R))$$$

Lean4

instance : Star (unitary R) :=
  ⟨fun U => ⟨star U, star_mem U.prop⟩⟩

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

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

Разделы

Аффилиация

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