[Merged by Bors] - refactor(FDeriv): use structure

[urkud]

This way we can easily change the definition so that it works for topological vector spaces without generalizing any of the theorems right away.

---

• depends on: [Merged by Bors] - chore(*Deriv*): golf #8899

[eric-wieser]

This way we can easily change the definition so that it works for topological vector spaces without generalizing any of the theorems right away.

What do you mean by this? Are you envisaging replacing it with a different structure? If so, the .1s and mks you use in the proof should probably be referred to by name and called of_isLittleO, respectively.

[urkud]

This way we can easily change the definition so that it works for topological vector spaces without generalizing any of the theorems right away.

What do you mean by this? Are you envisaging replacing it with a different structure?

Yes, I want to generalize the definition so that it works for maps between topological vector spaces, without generalizing all the lemmas immediately.

If so, the .1s and mks you use in the proof should probably be referred to by name and called of_isLittleO, respectively.

You're right and I was lazy. Fixed.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(*Deriv*): golf #8899
  By Dependent Issues (🤖). Happy coding!

[sgouezel]

bors r+
I've wanted to refactor derivatives for a long time, so if this helps you do it it's definitely a move in the right direction!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Check all files imported