smul_zpow — Mathlib

English

Let G act on H and H be a group, with a scalar-tower structure. Then for every g ∈ G, a ∈ H and integer n, (g • a)^{n} = g^{n} • a^{n}.

Русский

Пусть G действует на H, где H — группа, и имеется башня скаляров. Тогда для любого g ∈ G, a ∈ H и целого n: (g • a)^{n} = g^{n} • a^{n}.

LaTeX

$$$ (g \cdot a)^{n} = g^{n} \cdot a^{n} \quad (n \in \mathbb{Z}) $$$

Lean4

theorem smul_zpow (g : G) (a : H) (n : ℤ) : (g • a) ^ n = g ^ n • a ^ n := by cases n <;> simp [smul_pow, smul_inv]

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