instPow — Mathlib

English

If M is a Monoid with continuous multiplication, then SeparationQuotient M is equipped with a power operation for natural numbers.

Русский

Если M — моноид с непрерывным умножением, то SeparationQuotient(M) имеет возведение в степень по натуральным числам.

LaTeX

$$$\operatorname{Pow}(\mathrm{SeparationQuotient}(M), \mathbb{N})$$$

Lean4

@[to_additive existing instNSmul]
instance instPow [Monoid M] [ContinuousMul M] : Pow (SeparationQuotient M) ℕ where
  pow x n := Quotient.map' (s₁ := inseparableSetoid M) (· ^ n) (fun _ _ h ↦ Inseparable.pow h n) x

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