Commit 2024-04-16 20:19 a3653803
View on Github →feat(MeasureTheory/Haar): haarScalarFactor lemmas (#10383)
- Changed existing proofs of some lemmas to avoid code duplication. Took out some common lines in their proofs and turned them into a lemma.
haarScalarFactor \mu \mu = 1