instFintype

Mathlib.NumberTheory.LucasLehmer

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

English

There is a canonical coercion from Z/qZ to X_q given by the map [a] ↦ (a,0).

Русский

Существует каноническое отображение из Z/qZ в X_q, задаваемое отображением [a] ↦ (a,0).

LaTeX

$$$ \iota([a]) = (a,0) \quad \text{for all } a \in \mathbb{Z}/q\mathbb{Z}. $$$

Lean4

instance : Fintype (X q) :=
  inferInstanceAs (Fintype (ZMod q × ZMod q))

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

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

Разделы

Аффилиация

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