feat(linear_algebra/dimension): linear equiv iff eq dim (#5559)
See related zulip discussion
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Classification.20of.20finite-dimensional.20vector.20spaces/near/221357275
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
