Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dfinsupp.single_eq_pi_single

Modification history

2021-10-12 01:53
src/data/dfinsupp.lean
feat(data/dfinsupp, algebra/direct_sum/module): direct sum on fintype (#9664) …
Added dfinsupp.single_eq_pi_singleView on Github →