Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 19:11 5b774133

View on Github →

refactor(analysis/inner_product_space/pi_L2): change std_orthonormal_basis to type orthonormal_basis (#12253)

Estimated changes