Theorems · Theorem · ring theory

NonUnitalRingHom.map_closure

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

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

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRing