smul_pow' — Mathlib

English

Let M act on A as a distributive action. For all r ∈ M, x ∈ A, and n ∈ ℕ, r • x^n = (r • x)^n.

Русский

Пусть M действует на A как распределяющее действие. Тогда для всех r ∈ M, x ∈ A, n ∈ ℕ выполняется r • x^n = (r • x)^n.

LaTeX

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

Lean4

@[simp]
theorem smul_pow' (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n :=
  (MulDistribMulAction.toMonoidHom _ _).map_pow _ _

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