deficient

Mathlib.NumberTheory.FactorisationProperties

URI: https://scilib.ai/kg/mathlib#IsPrimePow.deficient

English

If n is a prime power, then n is deficient.

Русский

Если n является степенью простого, то n дефицитно.

LaTeX

$$$\operatorname{IsPrimePow}(n) \Rightarrow \operatorname{Deficient}(n)$$$

Lean4

theorem _root_.IsPrimePow.deficient (h : IsPrimePow n) : Deficient n :=
  by
  obtain ⟨p, k, hp, -, rfl⟩ := h
  exact hp.nat_prime.deficient_pow

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

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

Разделы

Аффилиация

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