Theorem DFinsupp.sum_mapRange_index.linearMap

Modification history

2024-02-04 23:05
Mathlib/LinearAlgebra/DFinsupp.lean
chore(LinearAlgebra,BigOperators): drop some decidability assumptions (#10237) …
Modified DFinsupp.sum_mapRange_index.linearMapView on Github →
2023-07-12 02:40
Mathlib/LinearAlgebra/DFinsupp.lean
chore: rename `Dfinsupp` to `DFinsupp` (#5822) …
Added DFinsupp.sum_mapRange_index.linearMapView on Github →