Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-18 02:05 b7572061

View on Github →

feat(linear_algebra/finite_dimensional): finrank_range_of_inj (#12067) The dimensions of the domain and range of an injective linear map are equal.

Estimated changes