Results about the cardinality of a quotient module.

theorem Submodule.card_eq_card_quotient_mul_card {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) : Nat.card M = Nat.card ↥S * Nat.card (M ⧸ S)