hasNatPow

Mathlib.RingTheory.WittVector.Truncated

URI: https://scilib.ai/kg/mathlib#TruncatedWittVector.hasNatPow

English

There is a natural-number power (Pow) on TruncatedWittVector defined by x^m = truncateFun(n)(x.out^m).

Русский

Существует показатель степени по натуральному числу на TruncatedWittVector: x^m = truncateFun(n)(x.out^m).

LaTeX

$$$ x^m = \mathrm{truncateFun}(n)(x.\mathrm{out})^{m} $$$

Lean4

instance hasNatPow : Pow (TruncatedWittVector p n R) ℕ :=
  ⟨fun x m => truncateFun n (x.out ^ m)⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru