Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 11:49 b1a9c2e4

View on Github →

feat(analysis/normed_space/multilinear): add norm_mk_pi_field (#10396) Also upgrade the corresponding equivalence to a linear_isometry.

Estimated changes