English
For n ≠ 0, the Finset {d ∈ range n.succ | d ∣ n} equals n.divisors.
Русский
Для n ≠ 0 множество {d ∈ range n.succ | d ∣ n} равно n.divisors.
LaTeX
$$$\{ d ∈ \mathrm{range}(n.succ) \mid d \mid n \} = \mathrm{divisors}(n)\quad (n \neq 0)$$$
Lean4
@[simp]
theorem filter_dvd_eq_divisors (h : n ≠ 0) : {d ∈ range n.succ | d ∣ n} = n.divisors :=
by
ext
simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)