fieldRange_comp_val — Mathlib

English

For a field F, an algebra hom f, the field range of the composition f.comp L is equal to the map of L by f.

Русский

Для поля F и алгебраического гомоморфа f, диапазон поля композиции f.comp L равен отображению L через f.

LaTeX

$$$(f.comp L.val).fieldRange = L.map f$$$

Lean4

theorem fieldRange_comp_val : (f.comp L.val).fieldRange = L.map f :=
  toSubalgebra_injective <| by rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]

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