X_mul_pderiv_monomial — Mathlib

English

Multiplying the derivative of a monomial by X_i yields the coefficient m_i times the original monomial.

Русский

Умножение производной мономиала на X_i даёт m_i умноженное на исходный мономиал.

LaTeX

$$$$ X_i \\cdot pderiv_i( monomial(m,r) ) = m(i) \\cdot monomial(m,r). $$$$

Lean4

theorem X_mul_pderiv_monomial {i : σ} {m : σ →₀ ℕ} {r : R} : X i * pderiv i (monomial m r) = m i • monomial m r :=
  by
  rw [pderiv_monomial, X, monomial_mul, smul_monomial]
  by_cases h : m i = 0
  · simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]
  rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]

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