factorization_eq_zero_of_remainder

English

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

Русский

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

LaTeX

$$$\\forall {n \\; p}: \\ Not(p \\mid n) \\rightarrow n.factorization(p) = 0$$$

Lean4

theorem factorization_eq_zero_of_remainder {p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) : (p * i + r).factorization p = 0 :=
  by
  apply factorization_eq_zero_of_not_dvd
  rwa [← Nat.dvd_add_iff_right (Dvd.intro i rfl)]

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