Commit 2020-11-21 21:24 79cd7204

View on Github →

feat(data/complex/is_R_or_C): Create a proper coercion from ℝ (#4824) This PR creates a proper coercion ℝ → 𝕜 for [is_R_or_C 𝕜], modelled on the code in data/nat/cast, as per the discussion here.

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

modified theorem inner_product_space.of_core.inner_norm_sq_eq_inner_self

modified theorem inner_product_space.of_core.inner_self_re_to_K

modified theorem inner_self_abs_to_K

modified theorem inner_self_re_to_K

Modified src/data/complex/is_R_or_C.lean

modified theorem is_R_or_C.abs_cast_nat

modified theorem is_R_or_C.abs_of_nonneg

modified theorem is_R_or_C.abs_of_real

modified theorem is_R_or_C.add_conj

added theorem is_R_or_C.coe_real_eq_id

modified theorem is_R_or_C.conj_mul_eq_norm_sq_left

modified theorem is_R_or_C.conj_of_real

modified theorem is_R_or_C.div_re_of_real

modified theorem is_R_or_C.eq_conj_iff_re

modified theorem is_R_or_C.eq_conj_iff_real

modified theorem is_R_or_C.int_cast_im

modified theorem is_R_or_C.int_cast_re

modified theorem is_R_or_C.inv_def

modified theorem is_R_or_C.mul_conj

modified theorem is_R_or_C.nat_cast_im

modified theorem is_R_or_C.nat_cast_re

modified theorem is_R_or_C.norm_sq_of_real

modified theorem is_R_or_C.of_real_add

modified theorem is_R_or_C.of_real_alg

modified theorem is_R_or_C.of_real_bit0

modified theorem is_R_or_C.of_real_bit1

modified theorem is_R_or_C.of_real_div

modified theorem is_R_or_C.of_real_eq_zero

added theorem is_R_or_C.of_real_finsupp_prod

added theorem is_R_or_C.of_real_finsupp_sum

modified theorem is_R_or_C.of_real_fpow

modified theorem is_R_or_C.of_real_im

modified theorem is_R_or_C.of_real_inj

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_mul_re

modified theorem is_R_or_C.of_real_nat_cast

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

added theorem is_R_or_C.of_real_prod

modified theorem is_R_or_C.of_real_rat_cast

modified theorem is_R_or_C.of_real_re

modified theorem is_R_or_C.of_real_sub

added theorem is_R_or_C.of_real_sum

deleted theorem is_R_or_C.of_real_to_complex

deleted theorem is_R_or_C.of_real_to_real

modified theorem is_R_or_C.of_real_zero

modified theorem is_R_or_C.rat_cast_im

modified theorem is_R_or_C.rat_cast_re

modified theorem is_R_or_C.re_add_im

modified theorem is_R_or_C.re_eq_add_conj

modified theorem is_R_or_C.smul_im

modified theorem is_R_or_C.smul_re

modified theorem is_R_or_C.sub_conj

deleted theorem is_R_or_C.zero_im

deleted theorem is_R_or_C.zero_re