Commit 2024-02-07 13:12 4daa227d

View on Github →

feat(MeasureTheory): product of bases and Basis.addHaar commute (#10115)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

added theorem Basis.prod_addHaar

added theorem Basis.prod_parallelepiped