mathlib3

4681620d - fix(analysis/inner_product_space): make type families explicit for `orthogonal_family` and `is_hilbert_sum` (#18584)

fix(analysis/inner_product_space): make type families explicit for `orthogonal_family` and `is_hilbert_sum` (#18584) Pretty much every single use of `orthogonal_family` was unable to infer this argument and so used `@`. `is_hilbert_sum` is changed for consistency.