Theorem FiniteDimensional.not_linearIndependent_of_infinite

Modification history

2023-12-18 12:58
Mathlib/LinearAlgebra/FiniteDimensional.lean
chore: Generalize results on `finrank` to rings. (#8912) …
Deleted FiniteDimensional.not_linearIndependent_of_infiniteView on Github →
2023-12-17 14:38
Mathlib/LinearAlgebra/FiniteDimensional.lean
feat: A lin. indep. family of vectors in a fin. dim. space is finite (#9103) …
Modified FiniteDimensional.not_linearIndependent_of_infiniteView on Github →
2023-04-25 11:42
Mathlib/LinearAlgebra/FiniteDimensional.lean
feat: port LinearAlgebra.FiniteDimensional (#3466)
Added FiniteDimensional.not_linearIndependent_of_infiniteView on Github →