Commit 2022-12-12 09:04 85158adc

fix(analysis/normed_space/basic): add back computable module instance (#17813) This was added in #8164 but removed in #17804. This also removes noncomputable theory since in fact only one result in the file needed it!