mathlib

08c1fbc7 - chore(measure_theory/measure/finite_measure_weak_convergence): golf (#15576)