monomial_smul_apply — Mathlib

English

The smul action of a monomial is shift-preserving: monomial i r • single R j m = single R (i+j) (r • m).

Русский

Действие мононимиального множителя сохраняет сдвиг: monomial i r • single R j m = single R (i+j) (r • m).

LaTeX

$$monomial i r • single R j m = single R (i + j) (r • m)$$

Lean4

@[simp]
theorem monomial_smul_apply (i : ℕ) (r : R) (g : PolynomialModule R M) (n : ℕ) :
    (monomial i r • g) n = ite (i ≤ n) (r • g (n - i)) 0 := by
  induction g using PolynomialModule.induction_linear with
  | zero => simp only [smul_zero, zero_apply, ite_self]
  | add p q hp hq =>
    simp only [smul_add, add_apply, hp, hq]
    split_ifs
    exacts [rfl, zero_add 0]
  | single =>
    rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]
    grind

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