mathlib3
67e606ea - chore(linear_algebra/dimension): fix lemma names (#18747)

Commit
2 years ago
chore(linear_algebra/dimension): fix lemma names (#18747) This fixes some lemma names which use `rank` but are about `finrank`: * `rank_sup_add_rank_inf_eq` → `submodule.rank_sup_add_rank_inf_eq` * `rank_add_le_rank_add_rank` → `submodule.rank_add_le_rank_add_rank` * `submodule.rank_sup_add_rank_inf_eq` → `submodule.finrank_sup_add_finrank_inf_eq` * `submodule.rank_add_le_rank_add_rank` → `submodule.finrank_add_le_finrank_add_finrank`
Author
Parents
Loading