Commit 2025-01-20 16:09 8f68dc48

View on Github →

chore: rename ENNReal lemmas to mul_{left,right}_inj for consistency (#20880)

Estimated changes

Modified Mathlib/Data/ENNReal/Operations.lean

deleted theorem ENNReal.mul_eq_mul_left

deleted theorem ENNReal.mul_eq_mul_right

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

Modified Mathlib/Probability/Independence/ZeroOne.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean