minpoly_add_algebraMap_splits — Mathlib

English

Let x be integral over R, and suppose h: Splits (algebraMap R L) (minpoly R x). Then Splits (algebraMap K L) (minpoly K x) for any tower R ⊆ K ⊆ L.

Русский

Пусть x интегрирован над R и minpoly R x распадается в L; тогда minpoly K x распадается в L для любой башни R ⊆ K ⊆ L.

LaTeX

$$$\\text{Splits}(\\operatorname{algebraMap} R L, \\minpoly R x) \\Rightarrow \\text{Splits}(\\operatorname{algebraMap} K L, \\minpoly K x)$$$

Lean4

theorem minpoly_add_algebraMap_splits [Algebra K L] {x : L} (r : K) (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (x + algebraMap K L r)).Splits (algebraMap K L) := by
  simpa [minpoly.add_algebraMap] using g.comp_X_sub_C r

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