Commit 2020-11-18 12:44 aff77270

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.