aroots_mul — Mathlib

English

Nonzero product of polynomials has roots equal to the union of roots with multiplicities.

Русский

Непустой произведение полиномов имеет корни, равные объединению корней с кратностями.

LaTeX

$$$\text{(Nonzero product)} \Rightarrow (p * q).aroots S = p.aroots S + q.aroots S$$$

Lean4

theorem aroots_mul [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p q : T[X]} (hpq : p * q ≠ 0) :
    (p * q).aroots S = p.aroots S + q.aroots S :=
  by
  suffices map (algebraMap T S) p * map (algebraMap T S) q ≠ 0 by rw [aroots_def, Polynomial.map_mul, roots_mul this]
  rwa [← Polynomial.map_mul, Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]

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