Zulip Chat Archive

Stream: maths

Topic: Haar measures


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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