Theorems · Theorem · ring theory

NonUnitalRingHom.map_sclosure

∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : Set R),
  NonUnitalSubsemiring.map f (NonUnitalSubsemiring.closure s) = NonUnitalSubsemiring.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.RingTheory.NonUnitalSubsemiring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringFunLikeNonUnitalNonAssocSemiringNonUnitalRingHomClass