Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 21:46 08c1fbc7

View on Github →

chore(measure_theory/measure/finite_measure_weak_convergence): golf (#15576)

Estimated changes