mathlib

9191c40c - feat(data/nat/factorization/basic): lemmas on divisibility of `ord_proj` and `ord_compl` (#15793)

feat(data/nat/factorization/basic): lemmas on divisibility of `ord_proj` and `ord_compl` (#15793) For `a b : ℕ`, we have `a ∣ b` iff * `∀ p : ℕ, ord_proj[p] a ∣ ord_proj[p] b` (for `a`, `b` positive) * `∀ p : ℕ, ord_compl[p] a ∣ ord_compl[p] b`