one_mem_toNonUnitalStarSubalgebra

Mathlib.Algebra.Star.Subalgebra

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

English

Multiplicative closure under the forgetting map to nonunital subalgebras.

Русский

Замыкание по умножению при переходе к неединичному подалгебренному.

LaTeX

$$$\\forall x,y\\in S, xy\\in S \\implies xy \\in S^{\\toNonUnitalStarSubalgebra}$$$

Lean4

theorem one_mem_toNonUnitalStarSubalgebra (S : StarSubalgebra R A) : 1 ∈ S.toNonUnitalStarSubalgebra :=
  S.one_mem'

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

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

Разделы

Аффилиация

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