English
divisorsAntidiagonalList(n) is the list of pairs (a,b) with a·b = n; divisorsAntidiagonalList(0) = [].
Русский
divisorsAntidiagonalList(n) — список пар (a,b) таких, что a·b = n; divisorsAntidiagonalList(0) = [].
LaTeX
$$$\mathrm{divisorsAntidiagonalList}(n) = \text{List of } (a,b) \in \mathbb{N}^2 \mid a b = n$; ограничение $0$ даёт пустой список.$$
Lean4
@[simp]
theorem mem_divisorsAntidiagonal {x : ℕ × ℕ} : x ∈ divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0 :=
by
obtain ⟨a, b⟩ := x
simp only [divisorsAntidiagonal, mul_div_eq_iff_dvd, mem_filterMap, mem_Icc, one_le_iff_ne_zero,
Option.ite_none_right_eq_some, Option.some.injEq, Prod.ext_iff, and_left_comm, exists_eq_left]
constructor
· rintro ⟨han, ⟨ha, han'⟩, rfl⟩
simp [Nat.mul_div_eq_iff_dvd, han]
cutsat
· rintro ⟨rfl, hab⟩
rw [mul_ne_zero_iff] at hab
simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt
