Theorems · Definition · group theory

MulEquiv.subsemigroupMap

{M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (e : M ≃* N) → (S : Subsemigroup M) → ↥S ≃* ↥(Subsemigroup.map (↑e) S)

A MulEquiv φ between two semigroups M and N induces a MulEquiv between a subsemigroup S ≤ M and the subsemigroup φ(S) ≤ N. See MulHom.subsemigroupMap for a variant for MulHoms.

Defined in

Mathlib.Algebra.Group.Subsemigroup.Operations

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

MulMul