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

Estimated changes