monmial_pow — Mathlib

English

Raising a monomial to a power distributes the exponent to its degree and exponentiates the coefficient.

Русский

Возведение мономиала в степень распаковывает степень на произведение степеней и возводит коэффициент в степень.

LaTeX

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

Lean4

theorem monmial_pow (m : ℕ) (a : R) (n : ℕ) : (monomial m a) ^ n = monomial (n * m) (a ^ n) := by
  simpa [monomial] using MvPowerSeries.monmial_pow (Finsupp.single () m) a n

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