Commit 2021-10-20 09:53 24901dde

View on Github →

feat(linear_algebra/free_module/rank): rank of free modules (#9810) This file contains a basic API for the rank of free modules. We will add the results for finite free modules in a future PR.

Estimated changes

Created src/linear_algebra/free_module/rank.lean

added theorem module.free.rank_direct_sum

added theorem module.free.rank_eq_card_choose_basis_index

added theorem module.free.rank_finsupp'

added theorem module.free.rank_finsupp

added theorem module.free.rank_prod'

added theorem module.free.rank_prod

added theorem module.free.rank_tensor_product'

added theorem module.free.rank_tensor_product