Mathlib v3 is deprecated. Go to Mathlib v4

Theorem direct_sum.linear_equiv_fun_on_fintype_symm_coe

Modification history

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