factorization_eq_zero_iff — Mathlib

English

For any n and p, the p-th coordinate of n’s factorization is 0 exactly when p is not prime, or p does not divide n, or n = 0.

Русский

Для любых n и p p-й координата факторизации n равна нулю тогда и только если p не простое, или p не делит n, либо n = 0.

LaTeX

$$$\\forall n,p:\\; n.factorization(p) = 0 \\iff \\neg \\text{Prime}(p) \\lor \\neg (p \\mid n) \\lor n = 0$$$

Lean4

theorem factorization_eq_zero_iff (n p : ℕ) : n.factorization p = 0 ↔ ¬p.Prime ∨ ¬p ∣ n ∨ n = 0 := by
  simp_rw [← notMem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]

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