Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-13 05:15 d0804bae

View on Github →

feat(linear_algebra/invariant_basis_number): basic API lemmas (#7882)

Estimated changes

Modified src/algebra/module/linear_map.lean

added theorem linear_equiv.coe_symm_mk

Modified src/linear_algebra/basic.lean

modified theorem finsupp.linear_equiv_fun_on_fintype_single

added theorem finsupp.linear_equiv_fun_on_fintype_symm_coe

modified theorem finsupp.linear_equiv_fun_on_fintype_symm_single

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/finite_dimensional.lean

Modified src/linear_algebra/finsupp.lean

Modified src/linear_algebra/invariant_basis_number.lean

added theorem card_eq_of_lequiv

added theorem card_le_of_injective'

added theorem card_le_of_injective

added theorem card_le_of_surjective'

added theorem card_le_of_surjective