Plan on merging this to Mathlib? #2
Description
I found this to be very useful for my project. Any plans on implementing this in Mathlib? Would Mathlib maintainers say yes to something so analysis?
{{ message }}
I found this to be very useful for my project. Any plans on implementing this in Mathlib? Would Mathlib maintainers say yes to something so analysis?