sum_divisors_eq_sum_properDivisors_add_self

English

For any n, the sum of all divisors equals the sum of proper divisors plus n.

Русский

Для любого n сумма всех делителей равна сумме собственных делителей плюс n.

LaTeX

$$$ \sum_{i \in \mathrm{divisors}(n)} i \\ = \\Big(\sum_{i \in \mathrm{properDivisors}(n)} i\Big) + n$$$

Lean4

theorem sum_divisors_eq_sum_properDivisors_add_self : ∑ i ∈ divisors n, i = (∑ i ∈ properDivisors n, i) + n :=
  by
  rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  · rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

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