theorem LinearMap.charpoly_degree {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) [StrongRankCondition R] : f.charpoly.degree = ↑(Module.finrank R M)