rq_eq

Mathlib.Data.PNat.Xgcd

URI: https://scilib.ai/kg/mathlib#PNat.XgcdType.rq_eq

English

The division with remainder relation holds: a = bp + 1 times q plus r, i.e., r + (bp + 1) q = ap + 1.

Русский

Отношение деления с остатком: a = (bp+1) q + r, т.е. r + (bp+1) q = a, где a = ap+1.

LaTeX

$$$u.r + (u.bp + 1) \\cdot u.q = u.ap + 1$$$

Lean4

/-- Properties of division with remainder for a / b. -/
theorem rq_eq : u.r + (u.bp + 1) * u.q = u.ap + 1 :=
  Nat.mod_add_div (u.ap + 1) (u.bp + 1)

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

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

Разделы

Аффилиация

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