English
For every natural n, divisorsAntidiag(ofNat(n)) is the disjoint union of the images of n.divisorsAntidiagonal under the two maps: (natCast, natCast) and (negNatCast, negNatCast).
Русский
Для каждого натурального n антидиагональ делителей(ofNat(n)) является дизъюнктным объединением образов n.divisorsAntidiagonal по двум отображениям: (natCast, natCast) и (negNatCast, negNatCast).
LaTeX
$$$ divisorsAntidiag(ofNat(n)) = (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by simp +contextual [disjoint_left, eq_comm]) $$$
Lean4
theorem divisorsAntidiag_ofNat (n : ℕ) :
divisorsAntidiag ofNat(n) =
(n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
(n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by simp +contextual [disjoint_left, eq_comm]) :=
rfl
