range — Mathlib

English

For a ring homomorphism f: R →+* S, the range is the subring of S consisting of all elements that are images of elements of R. Equivalently, Range(f) = Subring.map f ⊤.

Русский

Для кольцевого гомоморфизма f: R →+* S множество образа образует подкольцо в S; равенство Range(f) = Subring.map f ⊤.

LaTeX

$$$\\mathrm{range}(f) = \\mathrm{Subring.map}(f)(\\top)$$$

Lean4

/-- The range of a ring homomorphism, as a subring of the target. See Note [range copy pattern]. -/
def range {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : Subring S :=
  ((⊤ : Subring R).map f).copy (Set.range f) Set.image_univ.symm

Похожие утверждения