fieldRange — Mathlib

English

The range of a ring homomorphism f: K →+* L is a subfield of L.

Русский

Образ кольцевого однозначного гомоморфизма f: K →+* L является подполем L.

LaTeX

$$$ \mathrm{fieldRange}(f) \le \mathrm{Subfield}(L) $$$

Lean4

/-- The range of a ring homomorphism, as a subfield of the target. See Note [range copy pattern]. -/
def fieldRange : Subfield L :=
  ((⊤ : Subfield K).map f).copy (Set.range f) Set.image_univ.symm

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