divisorsAntidiag_natCast — Mathlib

English

A variant form expresses that negating the pair inside the index of divisorsAntidiag corresponds to membership equivalence; the pair (−x, −y) is in z.divisorsAntidiag iff (x, y) is.

Русский

Вариант формулировки: если взять пару (−x, −y) и проверить membership в z.divisorsAntidiag, то это эквивалентно membership пары (x, y).

LaTeX

$$$ (-x,-y) \in z.divisorsAntidiag \iff (x,y) \in z.divisorsAntidiag $$$

Lean4

theorem divisorsAntidiag_natCast (n : ℕ) :
    divisorsAntidiag n =
      (n.divisorsAntidiagonal.map <| .prodMap natCast natCast).disjUnion
        (n.divisorsAntidiagonal.map <| .prodMap negNatCast negNatCast) (by simp +contextual [disjoint_left, eq_comm]) :=
  rfl

Похожие утверждения