swap_mem_divisorsAntidiagonalList

English

For any pair a = (x, y), membership is preserved under swapping the components: a.swap ∈ n.divisorsAntidiagonalList iff a ∈ n.divisorsAntidiagonalList.

Русский

Для пары a = (x, y) членство сохраняется при замене местами компонент: a.swap ∈ n.divisorsAntidiagonalList ⇔ a ∈ n.divisorsAntidiagonalList.

LaTeX

$$$a.swap \\in n.divisorsAntidiagonalList \\iff a \\in n.divisorsAntidiagonalList$$$

Lean4

@[simp high]
theorem swap_mem_divisorsAntidiagonalList {a : ℕ × ℕ} :
    a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList := by simp [mul_comm]

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