Commit 2023-03-20 08:24 7307cd34

View on Github →

feat: port Algebra.DirectSum.Finsupp (#2995)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectSum/Finsupp.lean

added def finsuppLEquivDirectSum

added theorem finsuppLEquivDirectSum_single

added theorem finsuppLEquivDirectSum_symm_lof