filter_dvd_eq_divisors — Mathlib

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)

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