minpoly_algebraMap_sub_splits — Mathlib

English

Theorem: minpoly K (subtraction of algebraMap K L r from x) splits in L whenever minpoly K x splits in L.

Русский

Теорема: minpoly K (вычитание x и algebraMap K L r) распадается в L тогда и только если minpoly K x распадается в L.

LaTeX

$$$\\text{Splits}(\\operatorname{algebraMap} K L, \\minpoly K(x - \\operatorname{algebraMap} K L r))$$$

Lean4

theorem minpoly_algebraMap_sub_splits [Algebra K L] {x : L} (r : K) (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (algebraMap K L r - x)).Splits (algebraMap K L) := by
  simpa only [neg_sub] using minpoly_neg_splits (minpoly_sub_algebraMap_splits r g)

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