pow_eq_npowRec — Mathlib

English

For any submodule M and natural n, the n-th power M^n is equal to the iterated product defined by the recursive construction npowRec n M.

Русский

Для подмодуля M и натурального n равенство M^n = npowRec n M справедливо: n-я степень определяется как рекурсивное построение n раз перемножаемого подмодуля.

LaTeX

$$$M^n = \mathrm{npowRec}(n, M)$$$

Lean4

theorem pow_eq_npowRec {n : ℕ} : M ^ n = npowRec n M :=
  rfl

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