Commit 2026-03-02 23:05 e34f9275

chore(NumberTheory/ModularForms): golf using custom elaborators (#35730) The differential geometry directory gained some custom elaborators, which allow omitting the model with corners in many cases. For example, instead of writing MDifferentiable I J f, you can now write MDiff f (and I and J are usually inferred from the domain and co-domain of f --- if not, an error message will tell you why not). Use these elaborators to shorten differentiability statements.