Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-25 18:32 c544742c

View on Github →

feat(linear_algebra/finite_dimensional): add finrank_map_le (#8815)

Estimated changes

Modified src/linear_algebra/dimension.lean

added theorem linear_equiv.dim_map_eq

Modified src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.finrank_map_le

added theorem linear_equiv.finrank_map_eq