mathlib3

2c5d15de - Merge branch 'master' into dupuisf/linear_map_spectral