[Merged by Bors] - feat(category_theory/linear): linear functors

[semorrison]

---

• depends on: [Merged by Bors] - feat(category_theory): definition of R-linear category #7321

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(category_theory): definition of R-linear category #7321

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[b-mehta]

Other than my minor comment, this looks good to me!

[jcommelin]

We probably want definitions (or even instances?) that show that additive functors are always {nat,int,rat}-linear.
(We have things like add_monoid_hom.to_{nat,int,rat}_linear_map if I'm not mistaken. So this should be easy.
@semorrison do you want to add those to this PR? Or a follow-up?

[semorrison]

@jcommelin, done! I also relaxed some ring to semiring while I was at it, so we could actually say F.linear ℕ.

[jcommelin]

if CI-passes then
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests