English
For natural n, the divisors antidiagonal of (−n) equals the union of the images of n.divisorsAntidiagonal under the two sign patterns: (natCast, negNatCast) and (negNatCast, natCast).
Русский
Для натурального n антидиагональ делителей (−n) равна объединению образов n.divisorsAntidiagonal под двумя знаковыми образами: (natCast, negNatCast) и (negNatCast, natCast).
LaTeX
$$$ divisorsAntidiag(-n) = (n.divisorsAntidiagonal.map <| .prodMap natCast negNatCast).disjUnion (n.divisorsAntidiagonal.map <| .prodMap negNatCast natCast) (by simp +contextual [disjoint_left, eq_comm]) $$$
Lean4
theorem divisorsAntidiag_neg_natCast (n : ℕ) :
divisorsAntidiag (-n) =
(n.divisorsAntidiagonal.map <| .prodMap natCast negNatCast).disjUnion
(n.divisorsAntidiagonal.map <| .prodMap negNatCast natCast) (by simp +contextual [disjoint_left, eq_comm]) :=
by cases n <;> rfl
