Commit 2026-03-07 10:30 1a3385be

refactor(Distributions): remove "WithOrder" duplication (#36301) As explained in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Distribution/Distribution.html#Order-of-distributions, we consider test functions of finite regularities in order to track the change of regularities of certain operations (which in turns gives the order properties of the transpose operation at the level of distributions). To "hide" this to the user, my original approach was to duplicate everything: the WithOrder variant would track the regularities, while the default variant would just apply to smooth functions. @j-loreaux suggested avoiding some of this duplication by making the latter an abbreviation for the former. After some thoughts and discussion with @fpvandoorn, I came to the conclusion that we should just remove the specialization to the smooth case for now, as we will see later what is most convenient in practice.