mathlib3
3905fa80 - doc(measure_theory): Fix some names and docstrings (#18910)

Commit

2 years ago

doc(measure_theory): Fix some names and docstrings (#18910) Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>

Author

Felix-Weilacher

Parents