idIsPolyI'

Mathlib.RingTheory.WittVector.IsPoly

URI: https://scilib.ai/kg/mathlib#WittVector.idIsPolyI'

English

The identity function on Witt vectors is a polynomial function (variant).

Русский

Идентичность на Witt-векторах является полиномом (вариант).

LaTeX

$$$$IsPoly_p(\mathrm{id}).$$$$

Lean4

instance idIsPolyI' : IsPoly p fun _ _ a => a :=
  WittVector.idIsPoly _

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

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

Разделы

Аффилиация

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