feat(ring_theory/ideal): define `submodule.card_quot` (#17102)
This is the first step towards defining the absolute ideal norm: a definition of the cardinality of the quotient.
Once I've got a few more lemmas PR'd, we can show multiplicativity of `submodule.card_quot` restricted to ideals of a Dedekind domain, and bundle it into a `monoid_with_zero` hom.
