swap_mem_divisorsAntidiag — Mathlib

English

Let z be an integer and (x, y) a pair of integers. Then (x, y) lies in the antidiagonal divisors set of z if and only if (y, x) lies in the same set; i.e., the antidiagonal divisors are invariant under swapping coordinates.

Русский

Пусть z — целое число, и пары (x, y) из Z × Z принадлежат множеству делителей противодиагонали z тогда и только тогда, когда (y, x) принадлежит тому же множеству; антидиагональ делителей сохраняет симметрию при обмене координат.

LaTeX

$$$ \forall x,y,z \in \mathbb{Z},\; (x,y) \in z.divisorsAntidiag \iff (y,x) \in z.divisorsAntidiag $$$

Lean4

@[simp high]
theorem swap_mem_divisorsAntidiag : xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag := by simp [mul_comm]

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