pseudoperfect

Mathlib.NumberTheory.FactorisationProperties

URI: https://scilib.ai/kg/mathlib#Nat.Perfect.pseudoperfect

English

If n is perfect, then n is pseudoperfect.

Русский

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

LaTeX

$$$\operatorname{Perfect}(n) \rightarrow \operatorname{Pseudoperfect}(n)$$$

Lean4

theorem pseudoperfect (h : Perfect n) : Pseudoperfect n :=
  ⟨h.2, ⟨properDivisors n, ⟨fun ⦃_⦄ a ↦ a, h.1⟩⟩⟩

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

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

Разделы

Аффилиация

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