comap_id

Mathlib.Algebra.Star.Subalgebra

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

English

The preimage under the identity map is the original subalgebra: S.comap id = S.

Русский

Предобраз через тождественный отображение равен исходной подсалгебре: S.comap id = S.

LaTeX

$$$S.comap(\\mathrm{StarAlgHom.id}\\;R\\;A) = S$$$

Lean4

@[simp]
theorem comap_id (S : StarSubalgebra R A) : S.comap (StarAlgHom.id R A) = S :=
  SetLike.coe_injective <| Set.preimage_id

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

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

Разделы

Аффилиация

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