range_eq_top_of_surjective — Mathlib

English

If a ring homomorphism f: R →+* S is surjective, then its range is the entire codomain; i.e., f.range = ⊤.

Русский

Если гомоморфизм колец f: R →+* S сюръективен, то образ f равен всей кодоменой областью; то есть f.range = ⊤.

LaTeX

$$$ \\mathrm{Surjective}(f) \\Rightarrow f.\\mathrm{range} = (\\top : \\mathrm{Subring} S) $$$

Lean4

/-- The range of a surjective ring homomorphism is the whole of the codomain. -/
@[simp]
theorem range_eq_top_of_surjective (f : R →+* S) (hf : Function.Surjective f) : f.range = (⊤ : Subring S) :=
  range_eq_top.2 hf

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