zpow_apply — Mathlib

English

The coordinatewise definition of integer powers agrees with the global restriction: (x^n)_i = x_i^n for each i.

Русский

Координатное определение целочисленных степеней совпадает с глобальным: (x^n)_i = x_i^n.

LaTeX

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

Lean4

@[to_additive]
theorem zpow_apply [Π i, DivInvMonoid (R i)] [∀ i, SubgroupClass (S i) (R i)] (x : Πʳ i, [R i, B i]_[𝓕]) (n : ℤ)
    (i : ι) : (x ^ n) i = x i ^ n :=
  rfl

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