map_id

Mathlib.Algebra.Star.NonUnitalSubalgebra

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

English

Applying the identity map to a nonunital star-subalgebra yields the same subalgebra.

Русский

Применение тождесного отображения к неединичной звёздной подалгебре даёт ту же подалгебру.

LaTeX

$$\operatorname{map}(\mathrm{id},S) = S.$$

Lean4

@[simp]
theorem map_id (S : NonUnitalStarSubalgebra R A) : map (NonUnitalStarAlgHom.id R A) S = S :=
  SetLike.coe_injective <| Set.image_id _

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

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

Разделы

Аффилиация

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