mathlib3

ce3d53b0 - fix(data/real/basic): provide a computable `module` instance (#8164)

fix(data/real/basic): provide a computable `module` instance (#8164) Without this instance, `normed_field.to_normed_space` and `normed_space.to_module` is tried first, but this results in a noncomputable instance. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>