Commit 2024-02-06 09:06 7ab60686

View on Github →

chore(InnerProductSpace/Basic): drop some DecidableEq assumptions (#10291)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

modified theorem DFinsupp.inner_sum

modified theorem DFinsupp.sum_inner

modified theorem DirectSum.IsInternal.collectedBasis_orthonormal

modified theorem OrthogonalFamily.eq_ite

modified theorem OrthogonalFamily.inner_right_dfinsupp

modified theorem OrthogonalFamily.norm_sq_diff_sum

modified theorem orthonormal_iff_ite

modified theorem orthonormal_subtype_iff_ite