modPart_lt_p

Mathlib.NumberTheory.Padics.RingHoms

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

English

For any p, modPart(p,r) < p.

Русский

Для любого p modPart(p,r) < p.

LaTeX

$$$\\\\mathrm{modPart}(p,r) < p$$$

Lean4

theorem modPart_lt_p : modPart p r < p := by
  convert Int.emod_lt_abs _ _
  · simp
  · exact mod_cast hp_prime.1.ne_zero

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

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

Разделы

Аффилиация

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