mathlib3

fc3c0560 - chore(data/real): make more instances on real, nnreal, and ennreal computable (#9806)

chore(data/real): make more instances on real, nnreal, and ennreal computable (#9806) This makes it possible to talk about the add_monoid structure of nnreal and ennreal without worrying about computability. To make it clear exactly which operations are computable, we remove `noncomputable theory`.