mathlib3

3c95a727 - style(geometry/euclidean): consistently use inner product notation (#16961)

style(geometry/euclidean): consistently use inner product notation (#16961) Make `geometry.euclidean` files consistently use notation for the inner product, rather than mixing notation with non-notation calls to `inner`. Also always get that notation from `open_locale real_inner_product_space` instead of a local `notation` declaration.