Commit 2023-04-06 08:23 5aa3c1de

chore(linear_algebra/dimension): deduplicate lemmas (#18743) We have some lemmas in the module.free namespace which duplicate lemmas in the root namespace. This moves all the remaining rank lemmas in this namespace into the root namespace, and cleans up the overlapping lemmas this creates. The changes are:

• module.free.rank_eq_card_choose_basis_index: unchanged but moved to an earlier file
• rank_prod → rank_prod' (the non-universe polymorphic version)
• module.free.rank_prod → rank_prod
• none → rank_finsupp (new lemma)
• finsupp.rank_eq → rank_finsupp' (the non-universe polymorphic version)
• module.free.rank_finsupp → rank_finsupp_self
• module.free.rank_finsupp' → rank_finsupp_self' (the non-universe polymorphic version)
• module.free.rank_pi_finite → rank_pi (these were duplicates)
• For everything else, module.free.rank_* → rank_*