comap_id

Mathlib.Algebra.Group.Submonoid.Operations

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

English

Comap with the identity map is the same submonoid: S.comap (MonoidHom.id P) = S.

Русский

Прообраз при тождественном отображении равен самой подмономоде.

LaTeX

$$$ S^{comap\ id} = S $$$

Lean4

@[to_additive (attr := simp)]
theorem comap_id (S : Submonoid P) : S.comap (MonoidHom.id P) = S :=
  ext (by simp)

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

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

Разделы

Аффилиация

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