splits_of_splits_of_dvd — Mathlib

English

If f ≠ 0 and f splits, and g divides f, then g splits.

Русский

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

LaTeX

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

Lean4

theorem splits_of_splits_of_dvd {f g : K[X]} (hf0 : f ≠ 0) (hf : Splits i f) (hgf : g ∣ f) : Splits i g :=
  by
  obtain ⟨f, rfl⟩ := hgf
  exact (splits_of_splits_mul i hf0 hf).1

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