insert_self_properDivisors — Mathlib

English

For n ≠ 0, inserting n into its properDivisors yields divisors(n).

Русский

Для n ≠ 0 вставка n в properDivisors(n) даёт divisors(n).

LaTeX

$$$\mathrm{insert}\, n\, (\mathrm{properDivisors}(n)) = \mathrm{divisors}(n)\quad (n \neq 0)$$$

Lean4

theorem insert_self_properDivisors (h : n ≠ 0) : insert n (properDivisors n) = divisors n := by
  rw [divisors, properDivisors, ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h), Finset.filter_insert,
    if_pos (dvd_refl n)]

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