monomial_mul_X_pow — Mathlib

English

Let R be a semiring. For all n, k ∈ ℕ and r ∈ R, the product of the monomial of degree n with coefficient r and X^k equals the monomial of degree n+k with the same coefficient r.

Русский

Пусть R — полукольцо. Для любых n, k ∈ ℕ и r ∈ R произведение мономиала степени n с коэффициентом r на X^k равно мономиалу степени n+k с коэффициентом r.

LaTeX

$$$\mathrm{monomial}(n,r) \cdot X^{k} = \mathrm{monomial}(n+k,r)$$$

Lean4

@[simp]
theorem monomial_mul_X_pow (n : ℕ) (r : R) (k : ℕ) : monomial n r * X ^ k = monomial (n + k) r := by
  induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]

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