Cardinality of a module

This file proves that the cardinality of a module without zero divisors is at least the cardinality of its base ring.

theorem Cardinal.mk_le_of_module (R : Type u) (E : Type v) [AddCommGroup E] [Ring R] [Module R E] [Nontrivial E] [NoZeroSMulDivisors R E] : lift.{v, u} (mk R) ≤ lift.{u, v} (mk E)

The cardinality of a nontrivial module over a ring is at least the cardinality of the ring if there are no zero divisors (for instance if the ring is a field)