factorization): add lemma `factorization_le_iff_dvd` (#11377)

Commit

4 years ago

feat(data/nat/factorization): add lemma `factorization_le_iff_dvd` (#11377) For non-zero `d n : ℕ`, `d.factorization ≤ n.factorization ↔ d ∣ n`

Author

stuart-presnell

Parents