Theorems · Theorem · field theory

Polynomial.expand_aeval

∀ {R : Type u} [inst : CommSemiring R] {A : Type u_1} [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : ℕ)
  (P : Polynomial R) (r : A), (Polynomial.aeval r) ((Polynomial.expand R p) P) = (Polynomial.aeval (r ^ p)) P

Defined in

Mathlib.Algebra.Polynomial.Expand

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra