mulSingle_pow — Mathlib

English

Let (f i) be a family of monoids. For every i and x in f i and natural n, mulSingle i (x^n) = (mulSingle i x)^n.

Русский

Пусть для каждого i задан моноид f 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_pow [∀ i, Monoid (f i)] (i : I) (x : f i) (n : ℕ) : mulSingle i (x ^ n) = mulSingle i x ^ n :=
  (MonoidHom.mulSingle f i).map_pow x n

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