filter_dvd_eq_properDivisors — Mathlib

English

For n ≠ 0, the Finset {d ∈ range n | d ∣ n} equals n.properDivisors.

Русский

Для n ≠ 0, множество {d ∈ range n | d ∣ n} равно n.properDivisors.

LaTeX

$$$\{ d ∈ \mathrm{range}(n) \mid d \mid n \} = \mathrm{properDivisors}(n)\quad (n \neq 0)$$$

Lean4

@[simp]
theorem filter_dvd_eq_properDivisors (h : n ≠ 0) : {d ∈ range n | d ∣ n} = n.properDivisors :=
  by
  ext
  simp only [properDivisors, 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)

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