monmial_pow — Mathlib

English

For a multidegree m and a scalar a, (monomial m a)^n = monomial (n • m) (a^n).

Русский

Для многомерного многочлена m и скаляра a верна формула (monomial m a)^n = monomial (n • m) (a^n).

LaTeX

$$$(\\mathrm{monomial}\\ m\\ a)^n = \\mathrm{monomial}(n \\cdot m) (a^n)$$$

Lean4

theorem monmial_pow (m : σ →₀ ℕ) (a : R) (n : ℕ) : (monomial m a) ^ n = monomial (n • m) (a ^ n) := by
  rw [Finset.pow_eq_prod_const, prod_monomial, ← Finset.nsmul_eq_sum_const, ← Finset.pow_eq_prod_const]

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