mathlib

692b6b7c - chore(analysis/inner_product_space/basic): adjust decidability assumptions (#11212)

chore(analysis/inner_product_space/basic): adjust decidability assumptions (#11212) Eliminate the `open_locale classical` in `inner_product_space.basic` and replace by specific decidability assumptions.