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] [IsDomain R] [Module R E] [Nontrivial E] [Module.IsTorsionFree R E] : lift.{v, u} (mk R) ≤ lift.{u, v} (mk E)

The cardinality of a nontrivial torsion-free module over a domain is at least the cardinality of the ring.