Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-01 09:50 003141c8

View on Github →

chore(algebra/module): cleanup is_linear_map (#2296)

reuse facts about →+;
add map_smul
add a few docstrings

Estimated changes

Modified src/algebra/module.lean

modified theorem is_linear_map.map_add

modified theorem is_linear_map.map_neg

added theorem is_linear_map.map_smul

modified theorem is_linear_map.map_sub

modified theorem is_linear_map.map_zero

modified def linear_map.id