ordProj_pos

Mathlib.Data.Nat.Factorization.Basic

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

English

If a,b ≠ 0, then ordProj[p](a b) = ordProj[p] a · ordProj[p] b.

Русский

Если a ≠ 0 и b ≠ 0, то ordProj[p](a b) = ordProj[p] a · ordProj[p] b.

LaTeX

$$$ ordProj[p](a b) = ordProj[p] a \cdot ordProj[p] b $$$

Lean4

theorem ordProj_pos (n p : ℕ) : 0 < ordProj[p] n := by if pp : p.Prime then simp [Nat.pow_pos pp.pos] else simp [pp]

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

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

Разделы

Аффилиация

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