separable_gcd_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem separable_gcd_right {F : Type*} [Field F] [DecidableEq F[X]] {g : F[X]} (f : F[X]) (hg : g.Separable) :
    (EuclideanDomain.gcd f g).Separable :=
  Separable.of_dvd hg (EuclideanDomain.gcd_dvd_right f g)

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