sum_properDivisors_eq_one_iff_prime

English

For a natural number n, the sum of its proper divisors equals 1 if and only if n is prime.

Русский

Для натурального n сумма его правильных делителей равна 1 тогда и только тогда, когда n простое.

LaTeX

$$$\displaystyle \sum_{x \in n.properDivisors} x = 1 \iff n.Prime.$$$

Lean4

theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x = 1 ↔ n.Prime :=
  by
  rcases n with - | n
  · simp [Nat.not_prime_zero]
  · cases n
    · simp [Nat.not_prime_one]
    · rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2 (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

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