Abundant

Mathlib.NumberTheory.FactorisationProperties

URI: https://scilib.ai/kg/mathlib#Nat.Abundant

← MathLib Explorer

English

A natural number n is abundant if the sum of its proper divisors exceeds n.

Русский

Число натуральное n является чрезмерным, если сумма его proper divisors превосходит n.

LaTeX

$$n < ∑_{i ∈ properDivisors(n)} i$$

Lean4

/-- `n : ℕ` is _abundant_ if the sum of the proper divisors of `n` is greater than `n`. -/
def Abundant (n : ℕ) : Prop :=
  n < ∑ i ∈ properDivisors n, i

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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