minpoly_sub_algebraMap_splits — Mathlib

English

If g: minpoly K x splits in L, then minpoly K (x + algebraMap K L r) splits in L for any r ∈ K.

Русский

Если g: minpoly K x распадается в L, то minpoly K (x + algebraMap K L r) распадается в L для любого r ∈ K.

LaTeX

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

Lean4

theorem minpoly_sub_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 only [sub_eq_add_neg, map_neg] using minpoly_add_algebraMap_splits (-r) g

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