mathlib3
99fe12af - refactor(measure_theory/ae_eq_fun): move emetric to `ae_eq_fun_metric` (#6081)

Commit

4 years ago

refactor(measure_theory/ae_eq_fun): move emetric to `ae_eq_fun_metric` (#6081) Cherry-picked from #6042

Author

sgouezel

Parents