mathlib3

818dffa0 - feat(linear_algebra): a finite free module has a unique findim (#7631)

feat(linear_algebra): a finite free module has a unique findim (#7631) I needed this easy corollary, so I PR'd it, even though it should be generalizable once we have a better theory of e.g. Gaussian elimination. (I also tried to generalize `mk_eq_mk_of_basis`, but the current proof really requires the existence of multiplicative inverses for the coefficients.) Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>