Def DirectSum.linearEquivFunOnFintype

Modification history

2023-03-17 16:27

Mathlib/Algebra/DirectSum/Module.lean

feat: port Algebra.DirectSum.Module (#2596)

Added DirectSum.linearEquivFunOnFintype View on Github →