Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-01 10:36 1f39ada7

View on Github →

feat(linear_algebra): generalize linear_equiv.finrank_eq to rings (#12358) Since finrank doesn't assume the module is actually a vector space, neither should the statement that linear equivalences preserve it.

Estimated changes