subsemigroupComap

Mathlib.Algebra.Group.Subsemigroup.Operations

URI: https://scilib.ai/kg/mathlib#MulHom.subsemigroupComap

Lean4

/-- The `MulHom` from the preimage of a subsemigroup to itself. -/
@[to_additive (attr := simps) /-- The `AddHom` from the preimage of an additive subsemigroup to itself. -/
    ]
def subsemigroupComap (f : M →ₙ* N) (N' : Subsemigroup N) : N'.comap f →ₙ* N'
    where
  toFun x := ⟨f x, x.prop⟩
  map_mul' x y := Subtype.eq <| map_mul (M := M) (N := N) f x y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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