Commit 2024-01-12 18:56 56178f0a

feat(LinearAlgebra): generalize results about Module.rank of LinearMap. (#9677) LinearAlgebra/LinearIndependent: generalize linearIndependent_algHom_toLinearMap(') to allow different domain and codomain of the AlgHom. LinearAlgebra/Basic: add LinearEquiv.congrLeft that works for two rings with commuting actions on the codomain. LinearAlgebra/FreeModule/Finite/Matrix: generalize Module.Free.linearMap, Module.Finite.linearMap, and FiniteDimensional.finrank_linearMap to work with two different rings that may be noncommutative. Add FiniteDimensional.rank_linearMap, FiniteDimensional.(fin)rank_linearMap_self, and card/cardinal_mk_algHom_le_rank. FieldTheory/Tower: remove the instance LinearMap.finite_dimensional'' which becomes redundant; mark finrank_linear_map' as deprecated (superseded by finrank_linearMap_self.