not_abundant

Mathlib.NumberTheory.FactorisationProperties

URI: https://scilib.ai/kg/mathlib#Nat.Prime.not_abundant

English

If p is prime, then p is not abundant.

Русский

Если p простое, то p не является избыточным.

LaTeX

$$$\operatorname{Prime}(n) \rightarrow \lnot \operatorname{Abundant}(n)$$$

Lean4

theorem not_abundant (h : Prime n) : ¬Abundant n := fun h1 ↦
  (h.one_lt.trans h1).ne' (sum_properDivisors_eq_one_iff_prime.mpr h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru