separable_gcd_left — Mathlib

English

If f is a separable polynomial over a field F, then gcd(f,g) is separable for any g ∈ F[X].

Русский

Если f разделим над полем F, тогда gcd(f,g) разделим для любого g ∈ F[X].

LaTeX

$$$\\forall F,\\operatorname{Field}(F)\\,[\\text{DecidableEq}(F[X])] \\rightarrow (f\\Separable) \\Rightarrow \\operatorname{Separable}(\\gcd(f,g))$$$

Lean4

theorem separable_gcd_left {F : Type*} [Field F] [DecidableEq F[X]] {f : F[X]} (hf : f.Separable) (g : F[X]) :
    (EuclideanDomain.gcd f g).Separable :=
  Separable.of_dvd hf (EuclideanDomain.gcd_dvd_left f g)

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