modPart_nonneg

Mathlib.NumberTheory.Padics.RingHoms

URI: https://scilib.ai/kg/mathlib#PadicInt.modPart_nonneg

English

modPart(p,r) is nonnegative: 0 ≤ modPart(p,r).

Русский

modPart(p,r) неотрицателен: 0 ≤ modPart(p,r).

LaTeX

$$$0 \\le \\mathrm{modPart}(p,r)$$$

Lean4

theorem modPart_nonneg : 0 ≤ modPart p r :=
  Int.emod_nonneg _ <| mod_cast hp_prime.1.ne_zero

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

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

Разделы

Аффилиация

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