splits_of_splits_mul' — Mathlib

English

If Splits i f and Splits i g then Splits i (f * g).

Русский

Если Splits i f и Splits i g, то Splits i (f * g).

LaTeX

$$Splits i f → Splits i g → Splits i (f * g)$$

Lean4

theorem splits_of_splits_mul' {f g : K[X]} (hfg : (f * g).map i ≠ 0) (h : Splits i (f * g)) : Splits i f ∧ Splits i g :=
  ⟨Or.inr fun {g} hgi hg => Or.resolve_left h hfg hgi (by rw [Polynomial.map_mul]; exact hg.trans (dvd_mul_right _ _)),
    Or.inr fun {g} hgi hg => Or.resolve_left h hfg hgi (by rw [Polynomial.map_mul]; exact hg.trans (dvd_mul_left _ _))⟩

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