Theorems · Theorem · commutative algebra

RingHom.map_closureS

∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Set R),
  Subsemiring.map f (Subsemiring.closure s) = Subsemiring.closure (⇑f '' s)

The image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set.

Defined in

Mathlib.Algebra.Ring.Subsemiring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiring