splits_mul — Mathlib

English

If (f g).map i ≠ 0 and Splits i (f g), then Splits i f and Splits i g.

Русский

Если (f g).map i ≠ 0 и Splits i (f g), то Splits i f и Splits i g.

LaTeX

$$Ne (Polynomial.map i (f * g)) 0 → Splits i (f * g) → Splits i f ∧ Splits i g$$

Lean4

theorem splits_mul {f g : K[X]} (hf : Splits i f) (hg : Splits i g) : Splits i (f * g) :=
  letI := Classical.decEq L
  if h : (f * g).map i = 0 then Or.inl h
  else
    Or.inr fun {p} hp hpf =>
      ((irreducible_iff_prime.1 hp).2.2 _ _ (show p ∣ map i f * map i g by convert hpf; rw [Polynomial.map_mul])).elim
        (hf.resolve_left (fun hf => by simp [hf] at h) hp) (hg.resolve_left (fun hg => by simp [hg] at h) hp)

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