neg_mem_divisorsAntidiag — Mathlib

English

For any x, y, z ∈ Z, the membership of (−x, −y) in z.divisorsAntidiag is equivalent to the membership of (x, y) in z.divisorsAntidiag; i.e., negating both coordinates preserves membership in z.divisorsAntidiag.

Русский

Пусть x, y, z ∈ Z. Принадлежность пары (−x, −y) к z.divisorsAntidiag эквивалентна принадлежности (x, y) той же.antidiagonal; отрицание обеих координат сохраняет принадлежность.

LaTeX

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

Lean4

theorem neg_mem_divisorsAntidiag : -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag := by simp

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