Commit 2024-02-04 23:05 203b3966

View on Github →

chore(MeasureTheory/Cylinders): drop unneeded DecidableEq assumptions (#10254)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Cylinders.lean

modified theorem MeasureTheory.inter_cylinder_same

modified theorem MeasureTheory.union_cylinder_same