mathlib
ef093414 - chore(measure_theory/measure/haar_of_basis): axis-aligned parallepipeds are cuboids (#18829)

Commit
2 years ago
chore(measure_theory/measure/haar_of_basis): axis-aligned parallepipeds are cuboids (#18829) This was particularly annoying to prove; it feels like I might be missing some API somewhere. This also includes a result that @YaelDillies proved for me that shows a parallepiped can be formed by summing all the elements on its primary edges.
Author
Parents
Loading