ordCompl_pos

Mathlib.Data.Nat.Factorization.Basic

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

← MathLib Explorer

English

For all n,p, 0 < ordProj[p] n.

Русский

Для всех n,p: 0 < ordProj[p] n.

LaTeX

$$$ 0 < ordProj[p] n $$$

Lean4

theorem ordCompl_pos {n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < ordCompl[p] n := by
  if pp : p.Prime then exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
  else simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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