mathlib3

87861dd7 - feat(data/nat/factorization/basic): golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` (#15277)

feat(data/nat/factorization/basic): golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` (#15277) Golfs `card_multiples` ("exactly `n / p` naturals in `[1, n]` are multiples of `p`") and moves it from `data/nat/prime` to `data/nat/factorization/basic`. Also proves a slightly more convenient variant, `Ioc_filter_dvd_card_eq_div`.