monomial_pow — Mathlib

English

Raising a monomial to a power distributes: monomial(n,r)^k = monomial(n*k, r^k).

Русский

Возведение мономиала в степень распадается: monomial(n,r)^k = monomial(nk, r^k).

LaTeX

$$$\operatorname{monomial}(n,r)^{k} = \operatorname{monomial}(n\cdot k, r^{k})$$$

Lean4

@[simp]
theorem monomial_pow (n : ℕ) (r : R) (k : ℕ) : monomial n r ^ k = monomial (n * k) (r ^ k) := by
  induction k with
  | zero => simp [pow_zero, monomial_zero_one]
  | succ k ih => simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

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