snd_intCast

Mathlib.NumberTheory.LucasLehmer

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

English

For every integer n, the second coordinate of its image in X_q is zero: (n : X_q).snd = 0 in ZMod q.

Русский

Для каждого целого n вторая координата изображения n в X_q равна нулю: (n : X_q).snd = 0 в ZMod q.

LaTeX

$$$ (n : X q).snd = (0 : ZMod q) $$$

Lean4

@[simp]
theorem snd_intCast (n : ℤ) : (n : X q).snd = (0 : ZMod q) :=
  rfl

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

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

Разделы

Аффилиация

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