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] : LE.le (mk R).lift (mk E).lift

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)