X_pow_mul_monomial — Mathlib

English

For any k,n ∈ ℕ and r ∈ R, X^k multiplied by the monomial of degree n with coefficient r equals the monomial of degree n+k with coefficient r.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem X_pow_mul_monomial (k n : ℕ) (r : R) : X ^ k * monomial n r = monomial (n + k) r := by
  rw [X_pow_mul, monomial_mul_X_pow]

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