Commit 2023-05-04 11:37 338fe44f
View on Github →feat(data/is_R_or_C/basic): drop 2 fields, golf (#18931)
- Drop fields
inv_def_ax
anddiv_I_ax
inis_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
andis_R_or_C.coe_hom
. - Drop
is_R_or_C.inv_zero
andis_R_or_C.mul_inv_cancel
. - Move some lemmas to more appropriate sections.