Theorems · Theorem · commutative algebra

Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C

∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Multiset A)
  {x : A},
  x ∈ s →
    ∀ {p : Polynomial R},
      (Polynomial.mapAlg R A) p = (Multiset.map (fun x => Polynomial.X - Polynomial.C x) s).prod →
        (Polynomial.aeval x) p = 0

Defined in

Mathlib.RingTheory.Polynomial.Tower

Cited by

2 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommRingAlgebra