instPowCoeNatOfSubmonoidClass — Mathlib

English

If each fiber is a Monoid, then the restricted product inherits a natural-power operation given coordinatewise: (x^n)_i = x_i^n for n ∈ N.

Русский

Если каждый F_i является моноидом, ограниченное произведение inherits операцию возведения в натуральную степень, координатно: (x^n)_i = x_i^n.

LaTeX

$$$ (x^n)_i = x_i^n \quad (\forall i, n \in \mathbb{N}). $$$

Lean4

@[to_additive existing instNSMul]
instance [Π i, Monoid (R i)] [∀ i, SubmonoidClass (S i) (R i)] : Pow (Πʳ i, [R i, B i]_[𝓕]) ℕ where
  pow x n := ⟨fun i ↦ x i ^ n, x.2.mono fun _ hi ↦ pow_mem hi n⟩

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