mathlib
003141c8 - chore(algebra/module): cleanup `is_linear_map` (#2296)

Commit

5 years ago

chore(algebra/module): cleanup `is_linear_map` (#2296) * reuse facts about `→+`; * add `map_smul` * add a few docstrings

References

Author

urkud

Parents