Commit 2023-03-21 21:51 0d835252

View on Github →

feat: port LinearAlgebra.InvariantBasisNumber (#3025)

Estimated changes

added theorem card_eq_of_linearEquiv
added theorem card_le_of_injective'
added theorem card_le_of_injective
added theorem card_le_of_surjective'
added theorem card_le_of_surjective
added theorem eq_of_fin_equiv
added theorem le_of_fin_injective
added theorem le_of_fin_surjective