Commit 2023-04-14 14:34 2870d41a

View on Github →

feat: port LinearAlgebra.FreeModule.Rank (#3377) This PR also fixes the order of universes in Cardinal.lift_lift.

Estimated changes

added theorem rank_directSum
added theorem rank_finsupp'
added theorem rank_finsupp
added theorem rank_finsupp_self'
added theorem rank_finsupp_self
added theorem rank_matrix''
added theorem rank_matrix'
added theorem rank_matrix
added theorem rank_tensorProduct
added theorem rank_tensor_product'
deleted theorem Cardinal.lift_lift