Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-23 17:15 dfa95abf

View on Github →

feat(analysis/normed_space/linear_isometry): add an upgrade from linear isometries between finite dimensional spaces of eq finrank to linear isometry equivs (#8406)

Estimated changes