pow_add — Mathlib

English

If n ≠ 0, then M^(m+n) = M^m · M^n for natural numbers m, n; in particular, powers distribute over addition in the exponent when the second addend is nonzero.

Русский

Если n ≠ 0, то M^(m+n) = M^m · M^n для натуральных m, n; в частности, степени суммируются в показатель при ненулевом втором слагаемом.

LaTeX

$$$M^{(m+n)} = M^m \cdot M^n \quad (n \neq 0)$$$

Lean4

protected theorem pow_add {m n : ℕ} (h : n ≠ 0) : M ^ (m + n) = M ^ m * M ^ n :=
  npowRec_add m n h _ M.one_mul

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