q

Mathlib.Data.PNat.Xgcd

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

English

For a given XgcdType, q is defined as q = (ap + 1) / (bp + 1).

Русский

Для заданного XgcdType, q определяется как q = (ap + 1) / (bp + 1).

LaTeX

$$$ q = (ap(u) + 1) / (bp(u) + 1) $$$

Lean4

/-- `q = ap / bp`: quotient -/
def q : ℕ :=
  (u.ap + 1) / (u.bp + 1)

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

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

Разделы

Аффилиация

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