mulSingle_zpow — Mathlib

English

In a pi group with each component a group, for i ∈ I, x ∈ f i, and integer n, mulSingle i (x^n) = (mulSingle i x)^n.

Русский

В пи-группе, где каждая компонента является группой, для i∈I, x∈f i и целого n выполняется mulSingle i (x^n) = (mulSingle i x)^n.

LaTeX

$$$\mathrm{mulSingle}_i(x^n) = (\mathrm{mulSingle}_i x)^n$$$

Lean4

@[to_additive]
theorem mulSingle_zpow [∀ i, Group (f i)] (i : I) (x : f i) (n : ℤ) : mulSingle i (x ^ n) = mulSingle i x ^ n :=
  (MonoidHom.mulSingle f i).map_zpow x n

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