hasNatPow — Mathlib

English

There is a power operation on Witt vectors: for x in 𝕎_p(R) and n in ℕ, x^n is defined by x^n = eval (wittPow p n) (![x]).

Русский

Для Witt-вектора x и естественного числа n существует возведение в степень: x^n = eval (wittPow p n) (![x]).

LaTeX

$$$$ x^n = \mathrm{eval}\big(\mathrm{wittPow}(p, n)\big)(![x]). $$$$

Lean4

instance hasNatPow : Pow (𝕎 R) ℕ :=
  ⟨fun x n => eval (wittPow p n) ![x]⟩

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