English
Reversing the antidiagonal list corresponds to swapping coordinates in each pair: the reverse equals the list.map swap.
Русский
Разворот списка антидиагонали соответствует обмену координат в каждой паре: развёртывание списка равно списку, полученному применением swap ко всем парам.
LaTeX
$$$n.divisorsAntidiagonalList.reverse = n.divisorsAntidiagonalList.map .swap$$$
Lean4
theorem reverse_divisorsAntidiagonalList (n : ℕ) :
n.divisorsAntidiagonalList.reverse = n.divisorsAntidiagonalList.map .swap :=
by
have : IsAsymm (ℕ × ℕ) (·.snd < ·.snd) := ⟨fun _ _ ↦ lt_asymm⟩
refine
List.eq_of_perm_of_sorted ?_ sorted_divisorsAntidiagonalList_snd.reverse <|
sorted_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id
simp [List.reverse_perm',
List.perm_ext_iff_of_nodup nodup_divisorsAntidiagonalList (nodup_divisorsAntidiagonalList.map Prod.swap_injective),
mul_comm]
