Mathlib v3 is deprecated. Go to Mathlib v4

Def module.to_module_End

Modification history

2021-11-14 15:22

src/algebra/module/linear_map.lean

feat(data/equiv/module): add module.to_module_End (#10300) …

Added module.to_module_End View on Github →