Theorem DirectSum.sum_apply

Modification history

2026-03-25 04:00
Mathlib/Algebra/DirectSum/Basic.lean
chore(DirectSum): clean up instances (#37135) …
Added DirectSum.sum_applyView on Github →