hasPow — Mathlib

English

There is a natural-number exponentiation on NonemptyInterval α defined by repeated multiplication; s^n is the nth power with the induced multiplication.

Русский

Существует возведение в степень по натуральным значениям на NonemptyInterval α; s^n определяется повторным умножением.

LaTeX

$$$s^{n} \\text{ defined by } s^{n} = \\underbrace{s \\cdot (s \\cdot \\dots \\cdot s)}_{n\\text{ times}}$$$

Lean4

@[to_additive existing]
instance hasPow [MulLeftMono α] [MulRightMono α] : Pow (NonemptyInterval α) ℕ :=
  ⟨fun s n => ⟨s.toProd ^ n, pow_le_pow_left' s.fst_le_snd _⟩⟩

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