Theorem DFinsupp.inner_sum
Modification history
2024-08-30 00:21
Mathlib/Analysis/InnerProductSpace/Basic.lean
chore: rename Finsupp.total (#16277) …
Deleted DFinsupp.inner_sumView on Github →2024-02-06 09:06
Mathlib/Analysis/InnerProductSpace/Basic.lean
chore(InnerProductSpace/Basic): drop some `DecidableEq` assumptions (#10291)
Modified DFinsupp.inner_sumView on Github →