map

Mathlib.Algebra.Group.Subsemigroup.Operations

URI: https://scilib.ai/kg/mathlib#Subsemigroup.map

Lean4

/-- The image of a subsemigroup along a semigroup homomorphism is a subsemigroup. -/
@[to_additive /-- The image of an `AddSubsemigroup` along an `AddSemigroup` homomorphism is
          an `AddSubsemigroup`. -/
    ]
def map (f : M →ₙ* N) (S : Subsemigroup M) : Subsemigroup N
    where
  carrier := f '' S
  mul_mem' := by
    rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
    exact ⟨x * y, @mul_mem (Subsemigroup M) M _ _ _ _ _ _ hx hy, by rw [map_mul]⟩

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

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

Разделы

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

Аффилиация

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