Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-22 13:58 373911d5

View on Github →

chore(measure_theory): make μ an explicit argument in subsingleton.measure_zero etc (#8793)

Estimated changes

modified theorem measure_theory.dimH_empty
modified theorem finset.measure_zero
modified theorem set.countable.measure_zero
modified theorem set.finite.measure_zero