mersenne_coe_X

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.mersenne_coe_X

← MathLib Explorer

English

For any p, the mersenne number M_p maps to zero in X (q p).

Русский

Для любого p число Мерсенна M_p отображается в нуль в X(q p).

LaTeX

$$$ (\mathrm{mersenne}(p) : X (q p)) = 0 $$$

Lean4

/-- `q` is the minimum factor of `mersenne p`, so `M p = 0` in `X q`. -/
theorem mersenne_coe_X (p : ℕ) : (mersenne p : X (q p)) = 0 :=
  by
  ext <;> simp [mersenne, q, ZMod.natCast_eq_zero_iff, -pow_pos]
  apply Nat.minFac_dvd

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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