Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-06 10:56 13c41e1f

View on Github →

feat(category_theory/linear): linear functors (#7369)

Estimated changes

Modified src/category_theory/linear/default.lean

Created src/category_theory/linear/linear_functor.lean

added theorem category_theory.functor.coe_map_linear_map

added def category_theory.functor.map_linear_map

added theorem category_theory.functor.map_smul