factorization_eq_zero_of_not_dvd

Mathlib.Data.Nat.Factorization.Defs

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

English

If p does not divide n, then the p-th coordinate of n’s factorization is 0.

Русский

Если p не делит n, то соответствующая координата факторизации n равна 0.

LaTeX

$$$\\forall n,p:\\; \\neg(p \\mid n) \\Rightarrow n.factorization(p) = 0$$$

Lean4

theorem factorization_eq_zero_of_not_dvd {n p : ℕ} (h : ¬p ∣ n) : n.factorization p = 0 := by
  simp [factorization_eq_zero_iff, h]

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

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

Разделы

Аффилиация

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