mathlib3

85158adc - fix(analysis/normed_space/basic): add back computable module instance (#17813)

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!