Mathlib v3 is deprecated. Go to Mathlib v4

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 and div_I_ax in is_R_or_C, deduce them instead.
  • Use lemmas about ring_homs 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.

Estimated changes

modified theorem is_R_or_C.bit0_im
modified theorem is_R_or_C.bit0_re
modified theorem is_R_or_C.conj_bit0
modified theorem is_R_or_C.conj_bit1
modified theorem is_R_or_C.ext
modified theorem is_R_or_C.ext_iff
modified theorem is_R_or_C.inv_im
modified theorem is_R_or_C.of_real_add
modified theorem is_R_or_C.of_real_bit0
modified theorem is_R_or_C.of_real_eq_zero
modified theorem is_R_or_C.of_real_int_cast
modified theorem is_R_or_C.of_real_inv
modified theorem is_R_or_C.of_real_mul
modified theorem is_R_or_C.of_real_ne_zero
modified theorem is_R_or_C.of_real_neg
modified theorem is_R_or_C.of_real_one
modified theorem is_R_or_C.of_real_pow
modified theorem is_R_or_C.of_real_sub
modified theorem is_R_or_C.one_im
modified theorem is_R_or_C.one_re