instNatCast

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.X.instNatCast

English

There is a natural-number casting into X_q given by n ↦ (n,0).

Русский

Существует отображение натуральных чисел в X_q, n ↦ (n,0).

LaTeX

$$$\mathbb{N}\hookrightarrow X_q\, ,\ n\mapsto (n,0)$$$

Lean4

instance : NatCast (X q) where natCast := fun n => ⟨n, 0⟩

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

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

Разделы

Аффилиация

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