Theorem card_le_of_surjective'

Modification history

2023-08-10 19:52

Mathlib/LinearAlgebra/InvariantBasisNumber.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified card_le_of_surjective'View on Github →

2023-03-21 21:51

Mathlib/LinearAlgebra/InvariantBasisNumber.lean

feat: port LinearAlgebra.InvariantBasisNumber (#3025)

Added card_le_of_surjective'View on Github →