Theorem FiniteDimensional.rank_lt_of_finrank_lt

Modification history

2023-08-19 18:38

Mathlib/LinearAlgebra/Finrank.lean

feat(LinearAlgebra): complements on spaces of dimension >1 or >n (#6348)

Deleted FiniteDimensional.rank_lt_of_finrank_lt View on Github →

2023-04-12 20:56

Mathlib/LinearAlgebra/Finrank.lean

feat: port LinearAlgebra.Finrank (#3378)

Added FiniteDimensional.rank_lt_of_finrank_lt View on Github →