Dimension of trivial modules

@[simp]

theorem rank_subsingleton' (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] [Subsingleton M] : Module.rank R M = 0

See rank_subsingleton that assumes Subsingleton R instead.

theorem rank_punit (R : Type u_1) [Semiring R] [Nontrivial R] : Module.rank R PUnit.{u_3 + 1} = 0

theorem rank_bot (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] : Module.rank R ↥⊥ = 0