range — Mathlib

English

The range of a ring homomorphism from a local ring, viewed as a LocalSubring, is local.

Русский

Образ гомоморфизма из локального кольца, рассматриваемый как локальное подполь кольцо, локален.

LaTeX

$$IsLocalRing (LocalSubring.range f)$$

Lean4

/-- The range of a ring homomorphism from a local ring as a `LocalSubring`. -/
@[simps! toSubring]
def range [IsLocalRing R] [Nontrivial S] (f : R →+* S) : LocalSubring S :=
  .copy (map f (mk ⊤)) f.range (by ext x; exact congr(x ∈ $(Set.image_univ.symm)))

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