A module over a division ring is simple iff it has rank one

theorem isSimpleModule_iff_finrank_eq_one {R : Type u_1} {M : Type u_2} [DivisionRing R] [AddCommGroup M] [Module R M] : IsSimpleModule R M ↔ Module.finrank R M = 1