instPowNat — Mathlib

English

There is a natural-number power operation on regular expressions: P^n denotes the n-fold concatenation of P with itself.

Русский

Существует операция возведения регулярного выражения в степень по натуральному числу: P^n означает n-кратное конкатенирование P самой с собой.

LaTeX

$$$$ P^0 = \\varepsilon \\quad\\text{and}\\quad P^{n+1} = P^n \\cdot P \\quad (n \\in \\mathbb{N}). $$$$

Lean4

instance : Pow (RegularExpression α) ℕ :=
  ⟨fun n r => npowRec r n⟩

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