Nilpotent maps on finite modules

theorem Module.Finite.Module.End.isNilpotent_iff_of_finite {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] {f : End R M} : IsNilpotent f ↔ ∀ (m : M), ∃ (n : ℕ), (f ^ n) m = 0