fieldRange_eq_top_iff — Mathlib

English

For a field homomorphism f: K →+* L, the image f.fieldRange equals the top subfield ⊤ of L if and only if f is surjective.

Русский

Для гомоморфизма полей f: K →+* L образ f.fieldRange равен верхнему подполю ⊤ L тогда и только тогда, когда f сюръективен.

LaTeX

$$$f.fieldRange = \top \;\iff\; \mathrm{Surjective}(f)$$$

Lean4

theorem fieldRange_eq_top_iff {f : K →+* L} : f.fieldRange = ⊤ ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans Set.range_eq_univ

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