Commit 2023-12-27 04:42 fb6ba072

chore(LinearAlgebra): rename to enable LinearIndependent dot notation (#9144)

• Rename cardinal_lift_le_rank_of_linearIndependent, cardinal_le_rank_of_linearIndependent('), cardinal_mk/fintype_card/finset_card_le_finrank_of_linearIndependent, fintype_card_le_finrank_of_linearIndependent, finset_card_le_finrank_of_linearIndependent by removing trailing _of_linearIndependent in favor of namespace LinearIndependent.
• Remove cardinal_lift_le_rank_of_linearIndependent', exact duplicate of the version without the prime
• Rename FiniteDimensional/Module.Finite.lt_aleph0_of_linearIndependent to LinearIndependent.lt_aleph0_of_finiteDimensional/finite
• Add one lemma LinearIndependent.aleph0_le_rank in LinearAlgebra/Dimension and two lemmas LinearIndependent.finrank_eq_zero_of_infinite and finrank_eq_nat_card_basis in LinearAlgebra/Finrank
• Remove StrongRankCondition from finrank_eq_zero_of_basis_imp_not_finite and four subsequent lemmas