deficient_one

Mathlib.NumberTheory.FactorisationProperties

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

English

Deficient 1 holds, since 1 is deficient.

Русский

Deficient 1 выполняется, так как 1 дефектно (неполнено).

LaTeX

$$Deficient(1)$$

Lean4

theorem deficient_one : Deficient 1 :=
  zero_lt_one

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

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

Разделы

Аффилиация

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