Theorem FiniteDimensional.finite_of_finite

Modification history

2024-10-17 15:04
Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
feat: Over a finite ring, a module is finite iff it is finite dimensional (#17707) …
Deleted FiniteDimensional.finite_of_finiteView on Github →
2024-07-15 10:14
Mathlib/LinearAlgebra/FiniteDimensional.lean
chore: split LinearAlgebra.FiniteDimensional (#14670) …
Modified FiniteDimensional.finite_of_finiteView on Github →
2023-04-25 11:42
Mathlib/LinearAlgebra/FiniteDimensional.lean
feat: port LinearAlgebra.FiniteDimensional (#3466)
Added FiniteDimensional.finite_of_finiteView on Github →