Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-13 09:36 52d5fd47

View on Github →

feat(linear_algebra/{dimension,affine_space/finite_dimensional}): independent subsets of finite-dimensional spaces are finite. (#9674) Formalized as part of the Sphere Eversion project.

Estimated changes