Theorems · Theorem · commutative algebra

PolynomialModule.monomial_smul_apply

∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ) (r : R)
  (g : PolynomialModule R M) (n : ℕ), ((Polynomial.monomial i) r • g).coeff n = if i ≤ n then r • g.coeff (n - i) else 0

Defined in

Mathlib.Algebra.Polynomial.Module.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule