Theorems · Definition · group theory

Subsemigroup.comap

{M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → Subsemigroup N → Subsemigroup M

The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup.

Defined in

Mathlib.Algebra.Group.Subsemigroup.Operations

Cited by

39 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

MulMul