Mathlib v3 is deprecated. Go to Mathlib v4

Theorem card_le_of_injective'

Modification history

2021-08-13 05:15
src/linear_algebra/invariant_basis_number.lean
feat(linear_algebra/invariant_basis_number): basic API lemmas (#7882)
Added card_le_of_injective'View on Github →