mathlib3

b7572061 - feat(linear_algebra/finite_dimensional): finrank_range_of_inj (#12067)

feat(linear_algebra/finite_dimensional): finrank_range_of_inj (#12067) The dimensions of the domain and range of an injective linear map are equal. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>