starModule

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarSubalgebra.starModule

English

For a StarSubalgebra S, there is a corresponding NonUnitalStarSubalgebra forgetting the unit.

Русский

Для StarSubalgebra S существует соответствующая NonUnitalStarSubalgebra, забывающая единицу.

LaTeX

$$$S \\mapsto S^{\\toNonUnitalStarSubalgebra}$$$

Lean4

instance starModule (s : StarSubalgebra R A) : StarModule R s where star_smul r a := Subtype.ext (star_smul r (a : A))

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

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

Разделы

Аффилиация

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