Commit 2021-06-28 11:54 81183ea4

feat(geometry/manifold): derivation_bundle (#7708) In this PR we define the derivation_bundle. Note that this definition is purely algebraic and that the whole geometry/analysis is contained in the algebra structure of smooth global functions on the manifold. I believe everything runs smoothly and elegantly and that most proofs can be naturally done by rfl. To anticipate some discussions that already arose on Zulip about 9 months ago, note that the content of these files is purely algebraic and that there is no intention whatsoever to replace the current tangent bundle. I prefer this definition to the one given through the adjoint representation, because algebra is more easily formalized and simp can solve most proofs with this definition. However, in the future, there will be also the adjoint representation for sure.