reciprocalFactors — Mathlib

English

The reciprocalFactors(n) function produces a list of natural numbers describing a product of Dihedral groups whose commuting probability equals 1/n (constructed recursively).

Русский

Функция reciprocalFactors(n) порождает список натуральных чисел, задающих произведение диэдральных групп с commuting probability 1/n (конструируется рекурсивно).

LaTeX

$$\text{reciprocalFactors} : \mathbb{N} \to \text{List}(\mathbb{N})$$

Lean4

/-- A list of Dihedral groups whose product will have commuting probability `1 / n`. -/
def reciprocalFactors (n : ℕ) : List ℕ :=
  if _ : n = 0 then [0]
  else
    if _ : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)

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