splits_of_splits_gcd_right — Mathlib

English

If g ≠ 0 and g splits, then gcd(f,g) splits.

Русский

Если g ≠ 0 и g распадается, то gcd(f,g) распадается.

LaTeX

$$$g \neq 0 \land \operatorname{Splits}_i(g) \Rightarrow \operatorname{Splits}_i(\gcd(f,g))$$$

Lean4

theorem splits_of_splits_gcd_right [DecidableEq K] {f g : K[X]} (hg0 : g ≠ 0) (hg : Splits i g) :
    Splits i (EuclideanDomain.gcd f g) :=
  Polynomial.splits_of_splits_of_dvd i hg0 hg (EuclideanDomain.gcd_dvd_right f g)

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