Commit 2024-01-24 20:52 a686ba82

View on Github →

feat: finite products/sums of differentiable maps into smooth commutative monoids are differentiable (#9775) From sphere-eversion; I'm just upstreaming this.

Estimated changes