Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-17 11:19 3c95a727

View on Github →

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.

Estimated changes