Commit 2025-02-12 15:26 ba13a897

chore: make argument c implicit in of_measure_le_smul theorems (#21781) Make the argument c implement in {Integrable,MemLp}.of_measure_le_smul: both theorems take an argument c, immediately followed by a hypothesis hc about c: make c implicit. All applications in mathlib did not need to specify c.