English
An element a = (a1, a2) lies in n.divisorsAntidiagonalList exactly when a1 · a2 = n and n ≠ 0.
Русский
Элемент a = (a1, a2) принадлежит списку n.divisorsAntidiagonalList тогда и только тогда, когда a1 · a2 = n и n ≠ 0.
LaTeX
$$$a=(a_1,a_2)\\in n.divisorsAntidiagonalList\\iff a_1\\cdot a_2=n\\wedge n\\neq 0$$$
Lean4
@[simp]
theorem mem_divisorsAntidiagonalList {n : ℕ} {a : ℕ × ℕ} : a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0 := by
rw [← List.mem_toFinset, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonal]