Zulip Chat Archive
Stream: Is there code for X?
Topic: Existence of Haar measure from scratch
Dean Young (Nov 05 2023 at 04:51):
Is there a proof of the existence of Haar measure from scratch in Mathlib3/4? I was thinking about implementing one next year.
Scott Morrison (Nov 05 2023 at 05:02):
docs#MeasureTheory.Measure.haarMeasure
Last updated: May 02 2025 at 03:31 UTC