weird_seventy — Mathlib

English

Let n = 70. Then n is weird: it is abundant but not pseudoperfect.

Русский

Пусть n = 70. Это странное число: избыточное, но не псевдоперфектное.

LaTeX

$$$\\operatorname{Abundant}(70) \\land \\neg \\operatorname{Pseudoperfect}(70)$$$

Lean4

theorem weird_seventy : Weird 70 :=
  by
  rw [Weird, Abundant, not_pseudoperfect_iff_forall]
  have h : properDivisors 70 = { 1, 2, 5, 7, 10, 14, 35 } := by rfl
  constructor
  · rw [h]
    repeat norm_num
  · rw [h]
    right
    intro s hs
    have hs' := mem_powerset.mpr hs
    fin_cases hs' <;> decide

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