Theorems · Theorem · field theory

Polynomial.aeval_pi

∀ {R : Type u} [inst : CommSemiring R] {I : Type u_3} {A : I → Type u_4} [inst_1 : (i : I) → Semiring (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] (x : (i : I) → A i),
  Polynomial.aeval x = AlgHom.pi fun i => Polynomial.aeval (x i)

Polynomial evaluation on an indexed tuple is the indexed product of the evaluations on the components. Generalizes Polynomial.aeval_prod to indexed products.

Defined in

Mathlib.Algebra.Polynomial.AlgebraMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebra