not_pseudoperfect — Mathlib

English

If p is prime, then p is not pseudoperfect.

Русский

Если p простое, то p не псевдоперфектно.

LaTeX

$$$\operatorname{Prime}(p) \rightarrow \lnot \operatorname{Pseudoperfect}(p)$$$

Lean4

theorem not_pseudoperfect (h : Prime p) : ¬Pseudoperfect p :=
  by
  simp_rw [not_pseudoperfect_iff_forall, ← mem_powerset,
    show p.properDivisors.powerset = {∅, { 1 }} by rw [Prime.properDivisors h]; rfl]
  refine Or.inr (fun s hs ↦ ?_)
  fin_cases hs <;> simp only [sum_empty, sum_singleton] <;> linarith [Prime.one_lt h]

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