splits_of_splits_gcd_left — Mathlib

English

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

Русский

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

LaTeX

$$$f,g \in K[X],\ f \neq 0 \land \operatorname{Splits}_i(f) \Rightarrow \operatorname{Splits}_i(\gcd(f,g))$$$

Lean4

theorem splits_of_splits_gcd_left [DecidableEq K] {f g : K[X]} (hf0 : f ≠ 0) (hf : Splits i f) :
    Splits i (EuclideanDomain.gcd f g) :=
  Polynomial.splits_of_splits_of_dvd i hf0 hf (EuclideanDomain.gcd_dvd_left f g)

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