sMod_nonneg

Mathlib.NumberTheory.LucasLehmer

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

← MathLib Explorer

English

For p ≠ 0 and any i, sMod(p,i) is nonnegative as an integer.

Русский

Пусть p ≠ 0 и любой i. Тогда sMod(p,i) неотрицательно как целое число.

LaTeX

$$0 \le sMod(p,i)\quad(\text{для } p\neq 0)$$

Lean4

theorem sMod_nonneg (p : ℕ) (hp : p ≠ 0) (i : ℕ) : 0 ≤ sMod p i :=
  by
  cases i <;> dsimp [sMod]
  · exact sup_eq_right.mp rfl
  · apply Int.emod_nonneg
    exact mersenne_int_ne_zero p hp

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

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

Разделы

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

Аффилиация

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