Topic: Haar measures
Johan Commelin (Jul 24 2020 at 16:45):
@Floris van Doorn Do I understand correctly that you have material lying around for a 5th and final PR on Haar measures?
Floris van Doorn (Jul 24 2020 at 20:20):
I have to make some fixes and will PR it soon.
Floris van Doorn (Jul 24 2020 at 22:10):
I PR'd it: #3542
It still needs more documentation
Last updated: May 18 2021 at 08:14 UTC