mathlib3
94c141ac - chore(measure_theory/measurable_space_def): delete unused import (#17799)

Commit

3 years ago

chore(measure_theory/measurable_space_def): delete unused import (#17799)

Author

hrmacbeth

hrmacbeth

Parents

Loading