Commit 2023-06-01 10:18 906ce087

View on Github →

feat: port MeasureTheory.Measure.Haar.OfBasis (#4523)

Estimated changes

Modified Mathlib.lean

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

added theorem Basis.addHaar_self

added def Basis.parallelepiped

added theorem Basis.parallelepiped_map

added theorem Basis.parallelepiped_reindex

added theorem EuclideanSpace.coe_measurableEquiv

added theorem convex_parallelepiped

added theorem image_parallelepiped

added theorem mem_parallelepiped_iff

added def parallelepiped

added theorem parallelepiped_comp_equiv

added theorem parallelepiped_eq_convexHull

added theorem parallelepiped_eq_sum_segment

added theorem parallelepiped_orthonormalBasis_one_dim

added theorem parallelepiped_single