range_eq_top_of_surjective — Mathlib

English

The range of a surjective nonunital ring homomorphism is the whole codomain.

Русский

Образ сюръективного гомоморфизма без единицы равен всей кодомандой.

LaTeX

$$$\text{Surjective}(f) \Rightarrow f.range = \top$$$

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 = (⊤ : NonUnitalSubring S) :=
  range_eq_top.2 hf

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