map_fieldRange — Mathlib

English

If g: K →ₐ[F] L is an algebra hom and f: E →ₐ[F] K, then map g applied to f.fieldRange equals the fieldRange of the composition g ∘ f.

Русский

Образ g от поля области f равен полю области композиции g ∘ f.

LaTeX

$$$\operatorname{map} g (f.fieldRange) = (g \circ f).fieldRange$$$

Lean4

theorem _root_.AlgHom.map_fieldRange {L : Type*} [Field L] [Algebra F L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) :
    f.fieldRange.map g = (g.comp f).fieldRange :=
  SetLike.ext' (Set.range_comp g f).symm

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