Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-15 07:28 4681620d

View on Github →

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.

Estimated changes