Theorems · Theorem · field theory

Polynomial.reflect_C_mul

∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R) (r : R) (N : ℕ),
  Polynomial.reflect N (Polynomial.C r * f) = Polynomial.C r * Polynomial.reflect N f

Defined in

Mathlib.Algebra.Polynomial.Reverse

Cited by

2 results in Mathlib

Foundations

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

Assumes

Semiring