Theorems · Theorem · group theory

MulHom.map_mclosure

∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (s : Set M),
  Subsemigroup.map f (Subsemigroup.closure s) = Subsemigroup.closure (⇑f '' s)

The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup generated by the image of the set.

Defined in

Mathlib.Algebra.Group.Subsemigroup.Operations

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MulMul