coe_toNonUnitalStarSubalgebra

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra

English

The map of S equals the image S in the ambient set.

Русский

Отображение S через map соответствует образу S как множества.

LaTeX

$$map f S = f''S$$

Lean4

@[simp]
theorem coe_toNonUnitalStarSubalgebra (s : NonUnitalSubalgebra R A) (h_star) :
    (s.toNonUnitalStarSubalgebra h_star : Set A) = s :=
  rfl

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

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

Разделы

Аффилиация

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