pow_apply — Mathlib

English

Under a fiberwise Monoid structure, the nth power in the restricted product is coordinatewise: (x^n)_i = x_i^n.

Русский

При файловой моноидной структуре показатель степени действует по координатам: (x^n)_i = x_i^n.

LaTeX

$$$ (x^n)_i = x_i^n \quad (\forall i). $$$

Lean4

@[to_additive]
theorem pow_apply [Π i, Monoid (R i)] [∀ i, SubmonoidClass (S i) (R i)] (x : Πʳ i, [R i, B i]_[𝓕]) (n : ℕ) (i : ι) :
    (x ^ n) i = x i ^ n :=
  rfl

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