smul_pow — Mathlib

English

Under suitable SMulCommClass and IsScalarTower hypotheses, the scalar action commutes with taking powers: (r • x)^n = r^n • x^n for all n ∈ ℕ.

Русский

При подходящих гипотезах SMulCommClass и IsScalarTower скалярное действие взаимодействует со степенями: (r • x)^n = r^n • x^n.

LaTeX

$$$\\\\forall r \\\\in M, \\\\forall x \\\\in N, \\\\forall n \\\\in \\mathbb{N}, \\\\ (r \\\\cdot x)^n = r^n \\\\cdot x^n.$$$

Lean4

theorem smul_pow (r : M) (x : N) : ∀ n, (r • x) ^ n = r ^ n • x ^ n
  | 0 => by simp
  | n + 1 => by rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']

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