fst_intCast

Mathlib.NumberTheory.LucasLehmer

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

English

For every integer n, the first coordinate of its image in X_q equals its residue modulo q: (n : X_q).fst = (n : ZMod q).

Русский

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

LaTeX

$$$ (n : X q).fst = (n : ZMod q) $$$

Lean4

@[simp]
theorem fst_intCast (n : ℤ) : (n : X q).fst = (n : ZMod q) :=
  rfl

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

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

Разделы

Аффилиация

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