theorem div_left_injective₀ {G₀ : Type u_1} [CommGroupWithZero G₀] {c : G₀} (hc : c ≠ 0) : Function.Injective fun (x : G₀) => x / c

@[simp]

theorem Module.finrank_ne_zero {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [NoZeroSMulDivisors R M] [h : Nontrivial M] : finrank R M ≠ 0