toFinset_divisorsAntidiagonalList

English

The Finset obtained from divisorsAntidiagonalList via toFinset equals divisorsAntidiagonal.

Русский

Получившаяся Finset после преобразования divisorsAntidiagonalList в Finset равна divisorsAntidiagonal.

LaTeX

$$$\mathrm{toFinset}(n.\mathrm{divisorsAntidiagonalList}) = n.\mathrm{divisorsAntidiagonal}$$$

Lean4

@[simp]
theorem toFinset_divisorsAntidiagonalList {n : ℕ} : n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal := by
  rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap (f_inj := by simp_all),
    List.toFinset_range'_1_1]

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