Theorems · Theorem · group theory

AddHom.map_mclosure

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

The image under an AddSemigroup hom of the AddSubsemigroup generated by a set equals the AddSubsemigroup 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

AddAdd