natSepDegree_map — Mathlib

English

If i is a ring hom E → K between fields (with E and K suitably equipped as F-algebras), the separable degree of a polynomial f over E is preserved under map f ↦ f.map i.

Русский

Пусть i — кольцевой гомоморфизм E → K между полями, и f кольцевой над полем E. Тогда разделяемая степень f сохраняется под отображением f ↦ f.map i.

LaTeX

$$$ (f.\mathrm{map}\ i).\operatorname{natSepDegree} = f.\operatorname{natSepDegree} $$$

Lean4

theorem natSepDegree_map (f : E[X]) (i : E →+* K) : (f.map i).natSepDegree = f.natSepDegree := by
  classical
  let _ := i.toAlgebra
  simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K), aroots_def, map_map, ←
    IsScalarTower.algebraMap_eq]

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