Theorems · Definition · commutative algebra

RingHom.range

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

The range of a ring homomorphism, as a subring of the target. See Note [range copy pattern].

Defined in

Mathlib.Algebra.Ring.Subring.Basic

Cited by

138 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 339 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NonAssocRingNonAssocRing