swap_mem_divisorsAntidiagonal — Mathlib

English

The membership in divisorsAntidiagonal is invariant under swapping the coordinates.

Русский

При смене мест координат принадлежность к делителям антидиагонали сохраняется.

LaTeX

$$$ {x : \mathbb{N} \times \mathbb{N}}(x.swap \in divisorsAntidiagonal(n) \iff x \in divisorsAntidiagonal(n))$$$

Lean4

@[simp high]
theorem swap_mem_divisorsAntidiagonal {x : ℕ × ℕ} : x.swap ∈ divisorsAntidiagonal n ↔ x ∈ divisorsAntidiagonal n := by
  rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]

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