instFintype

Mathlib.RingTheory.WittVector.Truncated

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

English

If R is finite, then TruncatedWittVector p n R is finite, i.e., there is a finite type instance.

Русский

Если R конечен, то TruncatedWittVector p n R — конечного типа, существует соответствующий инстанс конечного типа.

LaTeX

$$$$\\text{Fintype }(\\mathrm{TruncatedWittVector}_p^n R). $$$$

Lean4

instance {R : Type*} [Fintype R] : Fintype (TruncatedWittVector p n R) :=
  Pi.instFintype

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

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

Разделы

Аффилиация

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