Weird

Mathlib.NumberTheory.FactorisationProperties

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

English

Weird(n) is equivalent to Abundant(n) ∧ ¬Pseudoperfect(n).

Русский

Weird(n) эквивалентно Abundant(n) ∧ ¬Pseudoperfect(n).

LaTeX

$$Weird(n) ↔ Abundant(n) ∧ ¬Pseudoperfect(n)$$

Lean4

/-- `n : ℕ` is a _weird_ number if and only if it is abundant but not pseudoperfect. -/
def Weird (n : ℕ) : Prop :=
  Abundant n ∧ ¬Pseudoperfect n

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

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

Разделы

Аффилиация

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