Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-06-04 09:53
1a62bb4c
View on Github →
feat(linear_algebra): strong rank condition implies rank condition (
#7683
)
Estimated changes
Modified
src/data/finsupp/basic.lean
added
theorem
finsupp.congr_fun
added
theorem
finsupp.equiv_fun_on_fintype_single
added
theorem
finsupp.equiv_fun_on_fintype_symm_single
Modified
src/linear_algebra/basic.lean
added
theorem
finsupp.linear_equiv_fun_on_fintype_single
added
theorem
finsupp.linear_equiv_fun_on_fintype_symm_single
Modified
src/linear_algebra/basis.lean
Modified
src/linear_algebra/finsupp.lean
added
theorem
linear_map.left_inverse_splitting_of_finsupp_surjective
added
theorem
linear_map.left_inverse_splitting_of_fun_on_fintype_surjective
added
def
linear_map.splitting_of_finsupp_surjective
added
theorem
linear_map.splitting_of_finsupp_surjective_injective
added
theorem
linear_map.splitting_of_finsupp_surjective_splits
added
def
linear_map.splitting_of_fun_on_fintype_surjective
added
theorem
linear_map.splitting_of_fun_on_fintype_surjective_injective
added
theorem
linear_map.splitting_of_fun_on_fintype_surjective_splits
Modified
src/linear_algebra/invariant_basis_number.lean