instNatCast

Mathlib.RingTheory.WittVector.Defs

URI: https://scilib.ai/kg/mathlib#WittVector.instNatCast

English

There is a natural embedding of natural numbers into Witt vectors: ℕ ↪ 𝕎_p(R).

Русский

Существует естественное вложение натуральных чисел в Witt-вектора: ℕ → 𝕎_p(R).

LaTeX

$$$$ \mathbb{N} \to \mathbb{W}_p(R). $$$$

Lean4

instance : NatCast (𝕎 R) :=
  ⟨Nat.unaryCast⟩

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

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

Разделы

Аффилиация

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