mathlib

c693682f - chore(analysis/normed/group/basic): make various norm instances computable (#9946)

chore(analysis/normed/group/basic): make various norm instances computable (#9946) Instead of defining the default `edist` as `ennreal.of_real` which introduces an `ite` on an undecidable equality, this constructs the `ennreal` directly using a proof of non-negativity. This removes `noncomputable theory` from some files so as to make it obvious from the source alone which definitions are and are not computable.