fieldRange_eq_map — Mathlib

English

For any f: E →ₐ[F] K, the field range is the image of the top intermediate field: f.fieldRange = map f ⊤.

Русский

Область значения гомоморфизма равна изображению верхнего промежуточного поля: fieldRange(f) = map f (⊤).

LaTeX

$$$f.fieldRange = \operatorname{map} f \top$$$

Lean4

theorem _root_.AlgHom.fieldRange_eq_map (f : E →ₐ[F] K) : f.fieldRange = IntermediateField.map f ⊤ :=
  SetLike.ext' Set.image_univ.symm

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