Theorem DFinsupp.zipWith_single_single

Modification history

2023-11-13 17:59
Mathlib/Data/DFinsupp/Basic.lean
fix(Mathlib/Algebra/Lie/DirectSum): remove unused `R` argument from lemmas (#8388) …
Added DFinsupp.zipWith_single_singleView on Github →