pow_succ' — Mathlib

English

For any submodule M and any n with n ≠ 0, M^{n+1} = M · M^{n}.

Русский

Для любого подмодуля M и натурального n, удовлетворяющего n ≠ 0, выполняется M^{n+1} = M · M^{n}.

LaTeX

$$$ M^{n+1} = M \cdot M^{n} \quad \text{for } n \ne 0. $$$

Lean4

/-- `Submodule.pow_succ` with the right-hand side commuted. -/
protected theorem pow_succ' {n : ℕ} (h : n ≠ 0) : M ^ (n + 1) = M * M ^ n := by
  rw [add_comm, M.pow_add h, Submodule.pow_one]

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