Commit 2021-05-01 09:09 55112757

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.