mem_divisorsAntidiagonalList — Mathlib

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]

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