fieldRange_eq_top — Mathlib

English

If f is an algebra equivalence E ≃ₐ[F] K, then the underlying AlgHom has top field range.

Русский

Если f -- алгебраическое эквивалентирование, то образ f как алгебраического гомоморфизма совпадает с верхним полем.

LaTeX

$$$\operatorname{fieldRange}(f) = \top$$$

Lean4

@[simp]
theorem _root_.AlgEquiv.fieldRange_eq_top (f : E ≃ₐ[F] K) : (f : E →ₐ[F] K).fieldRange = ⊤ :=
  AlgHom.fieldRange_eq_top.mpr f.surjective

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