mem_aroots — Mathlib

English

If p q ≠ 0, then the roots of p q over S are the multiset sum of the roots of p and q over S.

Русский

Если p q ≠ 0, то корни p q над S равны сумме множеств корней p и корней q над S.

LaTeX

$$aroots (p * q) S = aroots p S + aroots q S$$

Lean4

theorem mem_aroots [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {p : T[X]} {a : S} :
    a ∈ p.aroots S ↔ p ≠ 0 ∧ aeval a p = 0 :=
  by
  rw [mem_aroots', Polynomial.map_ne_zero_iff]
  exact FaithfulSMul.algebraMap_injective T S

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