feat(data/is_R_or_C/basic): drop 2 fields, golf (#18931)
* Drop fields `inv_def_ax` and `div_I_ax` in `is_R_or_C`, deduce them instead.
* Use lemmas about `ring_hom`s to prove properties of coercion, `is_R_or_C.re` etc.
* Drop `is_R_or_C.of_real_hom` and `is_R_or_C.coe_hom`.
* Drop `is_R_or_C.inv_zero` and `is_R_or_C.mul_inv_cancel`.
* Move some lemmas to more appropriate sections.
