English
DivisorsAntidiagonal(n) is the Finset of pairs (a,b) with a,b ∈ ℕ such that a · b = n; for 0 this set is empty.
Русский
DivisorsAntidiagonal(n) — множество пар \( (a,b) \) таких, что a,b ∈ ℕ и a·b = n; для 0 множество пусто.
LaTeX
$$$\mathrm{divisorsAntidiagonal}(n) = \{ (a,b) \in \mathbb{N} \times \mathbb{N} : a b = n \}$, с условием $0$ трактуется как пустое множество.$$
Lean4
/-- Pairs of divisors of a natural number as a finset.
`n.divisorsAntidiagonal` is the finset of pairs `(a, b) : ℕ × ℕ` such that `a * b = n`.
By convention, we set `Nat.divisorsAntidiagonal 0 = ∅`.
O(n). -/
def divisorsAntidiagonal : Finset (ℕ × ℕ) :=
(Icc 1 n).filterMap
(fun x ↦
let y := n / x;
if x * y = n then some (x, y) else none)
fun x₁ x₂ (x, y) hx₁ hx₂ ↦ by aesop
