properDivisors_eq_singleton_one_iff_prime

English

For any n, the proper divisors of n consist of the singleton {1} if and only if n is prime.

Русский

Для любого n правильные делители состоят из единицы тогда и только тогда, когда n — простое.

LaTeX

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

Lean4

theorem properDivisors_eq_singleton_one_iff_prime : n.properDivisors = { 1 } ↔ n.Prime :=
  by
  refine ⟨?_, ?_⟩
  · intro h
    refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩
    ·
      match n with
      | 0 => contradiction
      | 1 => contradiction
      | Nat.succ (Nat.succ n) => simp
    · rw [← mem_singleton, ← h, mem_properDivisors]
      have := Nat.le_of_dvd ?_ hdvd
      · simpa [hdvd, this] using (le_iff_eq_or_lt.mp this).symm
      · by_contra!
        simp only [nonpos_iff_eq_zero.mp this] at h
        contradiction
  · exact fun h => Prime.properDivisors h

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