multilinear): add `norm_mk_pi_field` (#10396)

Commit

4 years ago

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

Author

urkud

Parents