Commit 2023-04-08 20:46 45ce3929

View on Github →

chore(linear_algebra/dimension): tidy lemma names for linear_map.rank (#18769) le1 and le2 don't really fit the usual naming convention. Also generalizes rank_le_domain to rings and rank_le_range across universes.

Estimated changes

Modified src/data/matrix/rank.lean

Modified src/linear_algebra/dimension.lean

deleted theorem linear_map.rank_comp_le1

deleted theorem linear_map.rank_comp_le2

added theorem linear_map.rank_comp_le_left

added theorem linear_map.rank_comp_le_right

modified theorem linear_map.rank_le_range

Modified src/linear_algebra/matrix/to_lin.lean

modified theorem matrix.rank_vec_mul_vec