Commit 2021-10-25 17:43 c693682f

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.