pos

Mathlib.Algebra.IsPrimePow

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

English

If n is a prime power, then n > 0.

Русский

Если n является простой степенью, то n больше нуля.

LaTeX

$$IsPrimePow(n) \Rightarrow 0 < n$$

Lean4

theorem pos {n : ℕ} (hn : IsPrimePow n) : 0 < n :=
  pos_of_gt hn.two_le

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

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

Разделы

Аффилиация

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