minpoly_algebraMap_add_splits — Mathlib

English

If r ∈ K and g: (minpoly K x).Splits (algebraMap K L), then (minpoly K (x - algebraMap K L r)).Splits (algebraMap K L).

Русский

Если r ∈ K и g: (minpoly K x).Splits (algebraMap K L), то (minpoly K (x - algebraMap K L r)).Splits (algebraMap K L).

LaTeX

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

Lean4

theorem minpoly_algebraMap_add_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 [add_comm] using minpoly_add_algebraMap_splits r g

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