mem_toNonUnitalSubalgebra

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra

English

Membership to S.toNonUnitalSubalgebra is equivalent to membership to S.

Русский

Членство в S.toNonUnitalSubalgebra эквивалентно членству в S.

LaTeX

$$$x \\in S.toNonUnitalSubalgebra \\iff x \\in S$$$

Lean4

@[simp]
theorem mem_toNonUnitalSubalgebra {S : NonUnitalStarSubalgebra R A} {x} : x ∈ S.toNonUnitalSubalgebra ↔ x ∈ S :=
  Iff.rfl

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

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

Разделы

Аффилиация

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