Theorems · Definition · commutative algebra

Subring.map

{R : Type u} → {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (R →+* S) → Subring R → Subring S

The image of a subring along a ring homomorphism is a subring.

Defined in

Mathlib.Algebra.Ring.Subring.Basic

Cited by

33 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

NonAssocRingNonAssocRing