srangeRestrict

Mathlib.Algebra.Group.Subsemigroup.Operations

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

Lean4

/-- Restriction of a semigroup hom to its range interpreted as a subsemigroup. -/
@[to_additive /-- Restriction of an `AddSemigroup` hom to its range interpreted as a subsemigroup. -/
    ]
def srangeRestrict {N} [Mul N] (f : M →ₙ* N) : M →ₙ* f.srange :=
  (f.codRestrict f.srange) fun x => ⟨x, rfl⟩

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

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

Разделы

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

Аффилиация

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