Commit 2023-04-17 06:46 426149ac

View on Github →

chore: forward-port leanprover-community/mathlib#18784 (#3454)

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension.lean

added theorem LinearMap.lift_rank_comp_le

added theorem LinearMap.lift_rank_comp_le_right

added theorem LinearMap.rank_comp_le