Mathlib v3 is deprecated. Go to Mathlib v4

Def direct_sum.linear_equiv_fun_on_fintype

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 View on Github →