English
For any z and xy, xy ∈ divisorsAntidiag z iff xy.fst * xy.snd = z ∧ z ≠ 0.
Русский
Для любых z и пары xy, xy ∈ divisorsAntidiag z тогда и только тогда, когда xy.fst * xy.snd = z и z ≠ 0.
LaTeX
$$$\forall z\in\mathbb{Z},\ xy\in z.\mathrm{divisorsAntidiag} \iff xy.fst \cdot xy.snd = z \land z \neq 0.$$$
Lean4
/-- Pairs of divisors of an integer as a finset.
`z.divisorsAntidiag` is the finset of pairs `(a, b) : ℤ × ℤ` such that `a * b = z`.
By convention, we set `Int.divisorsAntidiag 0 = ∅`.
O(|z|). Computed from `Nat.divisorsAntidiagonal`. -/
def divisorsAntidiag : (z : ℤ) → Finset (ℤ × ℤ)
| (n : ℕ) =>
let s : Finset (ℕ × ℕ) := n.divisorsAntidiagonal
(s.map <| .prodMap natCast natCast).disjUnion (s.map <| .prodMap negNatCast negNatCast) <| by
simp +contextual [s, disjoint_left, eq_comm]
| negSucc n =>
let s : Finset (ℕ × ℕ) := (n + 1).divisorsAntidiagonal
(s.map <| .prodMap natCast negNatCast).disjUnion (s.map <| .prodMap negNatCast natCast) <| by
simp +contextual [s, disjoint_left, eq_comm, forall_swap (α := _ * _ = _)]
