mathlib3

aff77270 - chore(data/complex/is_R_or_C): Remove two unnecessary axioms (#5017)

chore(data/complex/is_R_or_C): Remove two unnecessary axioms (#5017) `of_real` and `smul_coe_mul_ax` are already implied by the algebra structure. The addition of `noncomputable` does not matter here, as both instances of `is_R_or_C` are marked non-computable anyway.