mathlib

ee8de4cf - doc(linear_algebra/finite_dimensional): update doc to new definition (#10758)

doc(linear_algebra/finite_dimensional): update doc to new definition (#10758) `finite_dimensional` is now (since a couple of months) defined to be `module.finite`. The lines modified by this PR are about the old definition.