Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-27 20:21 d360f3cb

View on Github →

feat(linear_algebra/free_module/finite/rank): add linear_algebra/free_module/finite/rank (#9832) A basic API for rank of free modules.

depends on: #9821

Estimated changes

Modified src/linear_algebra/dimension.lean

modified theorem dim_self

Modified src/linear_algebra/finite_dimensional.lean

Created src/linear_algebra/free_module/finite/rank.lean

added theorem module.free.finrank_direct_sum

added theorem module.free.finrank_eq_card_choose_basis_index

added theorem module.free.finrank_eq_rank

added theorem module.free.finrank_finsupp

added theorem module.free.finrank_linear_hom

added theorem module.free.finrank_matrix

added theorem module.free.finrank_pi

added theorem module.free.finrank_pi_fintype

added theorem module.free.finrank_prod

added theorem module.free.finrank_tensor_product

added theorem module.free.rank_lt_omega

Modified src/linear_algebra/free_module/rank.lean

modified theorem module.free.rank_direct_sum

added theorem module.free.rank_matrix''

added theorem module.free.rank_matrix'

added theorem module.free.rank_matrix

added theorem module.free.rank_pi_fintype

Modified src/set_theory/cardinal.lean

added theorem cardinal.to_nat_add_of_lt_omega

modified theorem cardinal.to_nat_mul