Zulip Chat Archive

Stream: maths

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):

Yes, it's here: https://github.com/leanprover-community/mathlib/blob/haar-measure2/src/measure_theory/haar_measure.leanZ

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: Dec 20 2023 at 11:08 UTC