Theorems · Theorem · commutative algebra

ascPochhammer_eval_comp

∀ {S : Type u} [inst : Semiring S] {R : Type u_1} [inst_1 : CommSemiring R] (n : ℕ) (p : Polynomial R)
  [inst_2 : Algebra R S] (x : S),
  Polynomial.eval x ((ascPochhammer S n).comp (Polynomial.map (algebraMap R S) p)) =
    Polynomial.eval (Polynomial.eval₂ (algebraMap R S) x p) (ascPochhammer S n)

Defined in

Mathlib.RingTheory.Polynomial.Pochhammer

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringCommSemiringAlgebra