smul_single_apply — Mathlib

English

The coefficient at n of (monomial i r) • g is given by r times g(n−i) if n≥i, otherwise 0.

Русский

Коэффициент при n у (monomial i r) • g равен r · g(n−i) при n≥i, иначе 0.

LaTeX

$$(monomial i r • g) n = if i ≤ n then r • g (n - i) else 0$$

Lean4

@[simp]
theorem smul_single_apply (i : ℕ) (f : R[X]) (m : M) (n : ℕ) :
    (f • single R i m) n = ite (i ≤ n) (f.coeff (n - i) • m) 0 := by
  induction f using Polynomial.induction_on' with
  | add p q hp hq =>
    rw [add_smul, Finsupp.add_apply, hp, hq, coeff_add, add_smul]
    split_ifs
    exacts [rfl, zero_add 0]
  | monomial => grind [monomial_smul_single, single_apply, coeff_monomial, zero_smul]

Похожие утверждения