instCoeZMod

Mathlib.NumberTheory.LucasLehmer

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

English

Defining ω as the element (2,1) in X_q.

Русский

Определение ω как элемента (2,1) в X_q.

LaTeX

$$$ \omega = (2,1) \in X_q $$$

Lean4

instance : Coe (ZMod ↑q) (X q) where coe := ZMod.castHom dvd_rfl (X q)

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

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

Разделы

Аффилиация

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