English
There is a bijection between divisors(n) and divisorsAntidiagonal(n) given by d ↦ (d, n/d).
Русский
Существуют биекция между делителями(n) и делителями антидиагонали(n) по $d \mapsto (d, n/d)$.
LaTeX
$$$ \mathrm{divisorsAntidiagonal}(n) = \{(d, n/d) : d \in \mathrm{divisors}(n)\} \quad (\text{при } n>0) $$$
Lean4
theorem map_div_right_divisors :
n.divisors.map ⟨fun d => (d, n / d), fun _ _ => congr_arg Prod.fst⟩ = n.divisorsAntidiagonal :=
by
ext ⟨d, nd⟩
simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors, Prod.ext_iff, and_left_comm,
exists_eq_left]
constructor
· rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩
rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
exact ⟨rfl, hn⟩
· rintro ⟨rfl, hn⟩
exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩
