Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.lift_symm_apply

Modification history

2021-02-16 23:59
src/linear_algebra/finsupp.lean
feat(algebra/category/Module): the free/forgetful adjunction for R-modules (#6168)
Added finsupp.lift_symm_applyView on Github →