finite_dimensional vector spaces are defined to be noetherian modules. Use finite_dimensional.of_fg to prove finite dimensional from a conventional definition.

The vector space of functions on a fintype has finite dimension.

The vector space of functions on a fintype ι has findim equal to the cardinality of ι.

The vector space of functions on fin n has findim equal to n.