ratio — Mathlib

English

A fixed internal ratio used in balancing decisions; ratio is defined as 2.

Русский

Фиксированное отношение, используемое при балансировочных решениях; ratio определяется как 2.

LaTeX

$$$\ratio := 2$$$

Lean4

/-- **Internal use only**

The ratio between an outer and inner sibling of the
heavier subtree in an unbalanced setting. It determines
whether a double or single rotation should be performed
to restore balance. It is corresponds with the inverse
of `α` in Adam's article. -/
@[inline]
def ratio :=
  2

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