mathlib3

55112757 - chore(measure_theory/ae_eq_fun_metric): remove useless file (#7419)

chore(measure_theory/ae_eq_fun_metric): remove useless file (#7419) The file `measure_theory/ae_eq_fun_metric.lean` used to contain an edistance on the space of equivalence classes of functions. It has been replaced by the use of the `L^1` space in #5510, so this file is now useless and should be removed.