English
DivisorsAntidiagonalList(n) is the list of pairs (a,b) with a·b = n, ordered by increasing a; by convention DivisorsAntidiagonalList(0) = [].
Русский
DivisorsAntidiagonalList(n) — список пар \( (a,b) \) с a·b = n, упорядоченный по возрастанию a; DivisorsAntidiagonalList(0) = [].
LaTeX
$$$\mathrm{divisorsAntidiagonalList}(n) = [ (a,b) \mid a b = n, a,b \in \mathbb{N}, a\le b, \text{ упорядочено по } a ]$ (с нулём как пустым списком).$$
Lean4
/-- Pairs of divisors of a natural number, as a list.
`n.divisorsAntidiagonalList` is the list of pairs `(a, b) : ℕ × ℕ` such that `a * b = n`, ordered
by increasing `a`. By convention, we set `Nat.divisorsAntidiagonalList 0 = []`.
-/
def divisorsAntidiagonalList (n : ℕ) : List (ℕ × ℕ) :=
(List.range' 1 n).filterMap
(fun x ↦
let y := n / x;
if x * y = n then some (x, y) else none)
