Commit 2024-03-28 10:26 43618f93

View on Github →

chore: Rename IsROrC to RCLike (#10819) IsROrC contains data, which goes against the expectation that classes prefixed with Is are prop-valued. People have been complaining about this on and off, so this PR renames IsROrC to RCLike.

Estimated changes

modified theorem Complex.conj_mul'
modified theorem Complex.inv_eq_conj
modified theorem Complex.mul_conj'
deleted theorem IsROrC.I_to_complex
deleted theorem IsROrC.conj_tsum
deleted theorem IsROrC.hasSum_conj'
deleted theorem IsROrC.hasSum_conj
deleted theorem IsROrC.hasSum_iff
deleted theorem IsROrC.hasSum_im
deleted theorem IsROrC.hasSum_ofReal
deleted theorem IsROrC.hasSum_re
deleted theorem IsROrC.im_eq_complex_im
deleted theorem IsROrC.im_to_complex
deleted theorem IsROrC.im_tsum
deleted theorem IsROrC.normSq_to_complex
deleted theorem IsROrC.ofReal_tsum
deleted theorem IsROrC.re_eq_complex_re
deleted theorem IsROrC.re_to_complex
deleted theorem IsROrC.re_tsum
deleted theorem IsROrC.summable_conj
deleted theorem IsROrC.summable_ofReal
added theorem RCLike.I_to_complex
added theorem RCLike.conj_tsum
added theorem RCLike.hasSum_conj'
added theorem RCLike.hasSum_conj
added theorem RCLike.hasSum_iff
added theorem RCLike.hasSum_im
added theorem RCLike.hasSum_ofReal
added theorem RCLike.hasSum_re
added theorem RCLike.im_to_complex
added theorem RCLike.im_tsum
added theorem RCLike.ofReal_tsum
added theorem RCLike.re_to_complex
added theorem RCLike.re_tsum
added theorem RCLike.summable_conj
added theorem RCLike.summable_ofReal
deleted def Inner.isROrCToReal
modified structure InnerProductSpace.Core
deleted theorem IsROrC.inner_apply
added theorem RCLike.inner_apply
modified theorem EuclideanSpace.dist_eq
modified theorem EuclideanSpace.edist_eq
modified theorem EuclideanSpace.nndist_eq
modified theorem EuclideanSpace.nnnorm_eq
modified theorem EuclideanSpace.norm_eq
deleted theorem IsROrC.norm_coe_norm
added theorem RCLike.norm_coe_norm
modified theorem spectrum.exp_mem_exp
deleted theorem IsROrC.I_im'
deleted theorem IsROrC.I_im
deleted theorem IsROrC.I_mul_I
deleted theorem IsROrC.I_mul_I_of_nonzero
deleted theorem IsROrC.I_mul_re
deleted theorem IsROrC.I_re
deleted theorem IsROrC.I_to_real
deleted theorem IsROrC.abs_im_le_norm
deleted theorem IsROrC.abs_re_le_norm
deleted theorem IsROrC.add_conj
deleted theorem IsROrC.bit0_im
deleted theorem IsROrC.bit0_re
deleted theorem IsROrC.bit1_im
deleted theorem IsROrC.bit1_re
deleted def IsROrC.conjAe
deleted theorem IsROrC.conjAe_coe
deleted theorem IsROrC.conjCLE_apply
deleted theorem IsROrC.conjCLE_coe
deleted theorem IsROrC.conjLIE_apply
deleted theorem IsROrC.conj_I
deleted theorem IsROrC.conj_bit0
deleted theorem IsROrC.conj_bit1
deleted theorem IsROrC.conj_div
deleted theorem IsROrC.conj_eq_iff_im
deleted theorem IsROrC.conj_eq_iff_re
deleted theorem IsROrC.conj_eq_iff_real
deleted theorem IsROrC.conj_eq_re_sub_im
deleted theorem IsROrC.conj_im
deleted theorem IsROrC.conj_inv
deleted theorem IsROrC.conj_mul
deleted theorem IsROrC.conj_neg_I
deleted theorem IsROrC.conj_ofReal
deleted theorem IsROrC.conj_re
deleted theorem IsROrC.conj_smul
deleted theorem IsROrC.conj_to_real
deleted theorem IsROrC.continuous_conj
deleted theorem IsROrC.continuous_im
deleted theorem IsROrC.continuous_normSq
deleted theorem IsROrC.continuous_ofReal
deleted theorem IsROrC.continuous_re
deleted theorem IsROrC.div_I
deleted theorem IsROrC.div_im
deleted theorem IsROrC.div_re
deleted theorem IsROrC.div_re_ofReal
deleted theorem IsROrC.ext
deleted theorem IsROrC.ext_iff
deleted theorem IsROrC.imCLM_apply
deleted theorem IsROrC.imCLM_coe
deleted def IsROrC.imLm
deleted theorem IsROrC.imLm_coe
deleted theorem IsROrC.im_eq_conj_sub
deleted theorem IsROrC.im_eq_zero
deleted theorem IsROrC.im_eq_zero_of_le
deleted theorem IsROrC.im_le_norm
deleted theorem IsROrC.im_ofReal_mul
deleted theorem IsROrC.im_sq_le_normSq
deleted theorem IsROrC.im_to_real
deleted theorem IsROrC.intCast_im
deleted theorem IsROrC.intCast_re
deleted theorem IsROrC.inv_I
deleted theorem IsROrC.inv_def
deleted theorem IsROrC.inv_eq_conj
deleted theorem IsROrC.inv_im
deleted theorem IsROrC.inv_re
deleted theorem IsROrC.isCauSeq_im
deleted theorem IsROrC.isCauSeq_norm
deleted theorem IsROrC.isCauSeq_re
deleted theorem IsROrC.is_real_TFAE
deleted theorem IsROrC.lt_iff_re_im
deleted theorem IsROrC.mul_conj
deleted theorem IsROrC.mul_im
deleted theorem IsROrC.mul_re
deleted theorem IsROrC.mul_self_norm
deleted theorem IsROrC.natCast_im
deleted theorem IsROrC.natCast_re
deleted theorem IsROrC.neg_iff
deleted theorem IsROrC.nonneg_iff
deleted theorem IsROrC.nonpos_iff
deleted def IsROrC.normSq
deleted theorem IsROrC.normSq_add
deleted theorem IsROrC.normSq_apply
deleted theorem IsROrC.normSq_conj
deleted theorem IsROrC.normSq_div
deleted theorem IsROrC.normSq_eq_def'
deleted theorem IsROrC.normSq_eq_zero
deleted theorem IsROrC.normSq_inv
deleted theorem IsROrC.normSq_mul
deleted theorem IsROrC.normSq_neg
deleted theorem IsROrC.normSq_nonneg
deleted theorem IsROrC.normSq_one
deleted theorem IsROrC.normSq_pos
deleted theorem IsROrC.normSq_sub
deleted theorem IsROrC.normSq_to_real
deleted theorem IsROrC.normSq_zero
deleted theorem IsROrC.norm_I_of_ne_zero
deleted theorem IsROrC.norm_conj
deleted theorem IsROrC.norm_im_le_norm
deleted theorem IsROrC.norm_natCast
deleted theorem IsROrC.norm_nsmul
deleted theorem IsROrC.norm_ofNat
deleted theorem IsROrC.norm_ofReal
deleted theorem IsROrC.norm_of_nonneg
deleted theorem IsROrC.norm_re_le_norm
deleted theorem IsROrC.norm_sq_eq_def
deleted theorem IsROrC.norm_two
deleted theorem IsROrC.ofNat_im
deleted theorem IsROrC.ofNat_mul_im
deleted theorem IsROrC.ofNat_mul_re
deleted theorem IsROrC.ofNat_re
deleted theorem IsROrC.ofRealAm_coe
deleted theorem IsROrC.ofRealCLM_apply
deleted theorem IsROrC.ofRealCLM_coe
deleted theorem IsROrC.ofRealLI_apply
deleted theorem IsROrC.ofReal_add
deleted theorem IsROrC.ofReal_alg
deleted theorem IsROrC.ofReal_bit0
deleted theorem IsROrC.ofReal_bit1
deleted theorem IsROrC.ofReal_div
deleted theorem IsROrC.ofReal_eq_zero
deleted theorem IsROrC.ofReal_finsupp_sum
deleted theorem IsROrC.ofReal_im
deleted theorem IsROrC.ofReal_inj
deleted theorem IsROrC.ofReal_injective
deleted theorem IsROrC.ofReal_intCast
deleted theorem IsROrC.ofReal_inv
deleted theorem IsROrC.ofReal_mul
deleted theorem IsROrC.ofReal_natCast
deleted theorem IsROrC.ofReal_ne_zero
deleted theorem IsROrC.ofReal_neg
deleted theorem IsROrC.ofReal_ofNat
deleted theorem IsROrC.ofReal_one
deleted theorem IsROrC.ofReal_pow
deleted theorem IsROrC.ofReal_prod
deleted theorem IsROrC.ofReal_ratCast
deleted theorem IsROrC.ofReal_re
deleted theorem IsROrC.ofReal_real_eq_id
deleted theorem IsROrC.ofReal_sub
deleted theorem IsROrC.ofReal_sum
deleted theorem IsROrC.ofReal_zero
deleted theorem IsROrC.ofReal_zpow
deleted theorem IsROrC.one_im
deleted theorem IsROrC.one_re
deleted theorem IsROrC.pos_iff
deleted theorem IsROrC.ratCast_im
deleted theorem IsROrC.ratCast_re
deleted theorem IsROrC.reCLM_apply
deleted theorem IsROrC.reCLM_coe
deleted def IsROrC.reLm
deleted theorem IsROrC.reLm_coe
deleted theorem IsROrC.re_add_im
deleted theorem IsROrC.re_eq_add_conj
deleted theorem IsROrC.re_eq_self_of_le
deleted theorem IsROrC.re_le_norm
deleted theorem IsROrC.re_ofReal_mul
deleted theorem IsROrC.re_sq_le_normSq
deleted theorem IsROrC.re_to_real
deleted theorem IsROrC.real_smul_ofReal
deleted theorem IsROrC.smul_im
deleted theorem IsROrC.smul_re
deleted theorem IsROrC.star_def
deleted theorem IsROrC.sub_conj
deleted theorem IsROrC.toOrderedSMul
deleted theorem IsROrC.zero_re'
added theorem RCLike.I_im'
added theorem RCLike.I_im
added theorem RCLike.I_mul_I
added theorem RCLike.I_mul_re
added theorem RCLike.I_re
added theorem RCLike.I_to_real
added theorem RCLike.abs_im_le_norm
added theorem RCLike.abs_re_le_norm
added theorem RCLike.add_conj
added theorem RCLike.bit0_im
added theorem RCLike.bit0_re
added theorem RCLike.bit1_im
added theorem RCLike.bit1_re
added def RCLike.conjAe
added theorem RCLike.conjAe_coe
added theorem RCLike.conjCLE_apply
added theorem RCLike.conjCLE_coe
added theorem RCLike.conjLIE_apply
added theorem RCLike.conj_I
added theorem RCLike.conj_bit0
added theorem RCLike.conj_bit1
added theorem RCLike.conj_div
added theorem RCLike.conj_eq_iff_im
added theorem RCLike.conj_eq_iff_re
added theorem RCLike.conj_im
added theorem RCLike.conj_inv
added theorem RCLike.conj_mul
added theorem RCLike.conj_neg_I
added theorem RCLike.conj_ofReal
added theorem RCLike.conj_re
added theorem RCLike.conj_smul
added theorem RCLike.conj_to_real
added theorem RCLike.continuous_conj
added theorem RCLike.continuous_im
added theorem RCLike.continuous_re
added theorem RCLike.div_I
added theorem RCLike.div_im
added theorem RCLike.div_re
added theorem RCLike.div_re_ofReal
added theorem RCLike.ext
added theorem RCLike.ext_iff
added theorem RCLike.imCLM_apply
added theorem RCLike.imCLM_coe
added def RCLike.imLm
added theorem RCLike.imLm_coe
added theorem RCLike.im_eq_conj_sub
added theorem RCLike.im_eq_zero
added theorem RCLike.im_le_norm
added theorem RCLike.im_ofReal_mul
added theorem RCLike.im_sq_le_normSq
added theorem RCLike.im_to_real
added theorem RCLike.intCast_im
added theorem RCLike.intCast_re
added theorem RCLike.inv_I
added theorem RCLike.inv_def
added theorem RCLike.inv_eq_conj
added theorem RCLike.inv_im
added theorem RCLike.inv_re
added theorem RCLike.isCauSeq_im
added theorem RCLike.isCauSeq_norm
added theorem RCLike.isCauSeq_re
added theorem RCLike.is_real_TFAE
added theorem RCLike.lt_iff_re_im
added theorem RCLike.mul_conj
added theorem RCLike.mul_im
added theorem RCLike.mul_re
added theorem RCLike.mul_self_norm
added theorem RCLike.natCast_im
added theorem RCLike.natCast_re
added theorem RCLike.neg_iff
added theorem RCLike.nonneg_iff
added theorem RCLike.nonpos_iff
added def RCLike.normSq
added theorem RCLike.normSq_add
added theorem RCLike.normSq_apply
added theorem RCLike.normSq_conj
added theorem RCLike.normSq_div
added theorem RCLike.normSq_eq_def'
added theorem RCLike.normSq_eq_zero
added theorem RCLike.normSq_inv
added theorem RCLike.normSq_mul
added theorem RCLike.normSq_neg
added theorem RCLike.normSq_nonneg
added theorem RCLike.normSq_one
added theorem RCLike.normSq_pos
added theorem RCLike.normSq_sub
added theorem RCLike.normSq_to_real
added theorem RCLike.normSq_zero
added theorem RCLike.norm_conj
added theorem RCLike.norm_im_le_norm
added theorem RCLike.norm_natCast
added theorem RCLike.norm_nsmul
added theorem RCLike.norm_ofNat
added theorem RCLike.norm_ofReal
added theorem RCLike.norm_of_nonneg
added theorem RCLike.norm_re_le_norm
added theorem RCLike.norm_sq_eq_def
added theorem RCLike.norm_two
added theorem RCLike.ofNat_im
added theorem RCLike.ofNat_mul_im
added theorem RCLike.ofNat_mul_re
added theorem RCLike.ofNat_re
added theorem RCLike.ofRealAm_coe
added theorem RCLike.ofRealCLM_apply
added theorem RCLike.ofRealCLM_coe
added theorem RCLike.ofRealLI_apply
added theorem RCLike.ofReal_add
added theorem RCLike.ofReal_alg
added theorem RCLike.ofReal_bit0
added theorem RCLike.ofReal_bit1
added theorem RCLike.ofReal_div
added theorem RCLike.ofReal_eq_zero
added theorem RCLike.ofReal_im
added theorem RCLike.ofReal_inj
added theorem RCLike.ofReal_intCast
added theorem RCLike.ofReal_inv
added theorem RCLike.ofReal_mul
added theorem RCLike.ofReal_natCast
added theorem RCLike.ofReal_ne_zero
added theorem RCLike.ofReal_neg
added theorem RCLike.ofReal_ofNat
added theorem RCLike.ofReal_one
added theorem RCLike.ofReal_pow
added theorem RCLike.ofReal_prod
added theorem RCLike.ofReal_ratCast
added theorem RCLike.ofReal_re
added theorem RCLike.ofReal_sub
added theorem RCLike.ofReal_sum
added theorem RCLike.ofReal_zero
added theorem RCLike.ofReal_zpow
added theorem RCLike.one_im
added theorem RCLike.one_re
added theorem RCLike.pos_iff
added theorem RCLike.ratCast_im
added theorem RCLike.ratCast_re
added theorem RCLike.reCLM_apply
added theorem RCLike.reCLM_coe
added def RCLike.reLm
added theorem RCLike.reLm_coe
added theorem RCLike.re_add_im
added theorem RCLike.re_eq_add_conj
added theorem RCLike.re_le_norm
added theorem RCLike.re_ofReal_mul
added theorem RCLike.re_sq_le_normSq
added theorem RCLike.re_to_real
added theorem RCLike.smul_im
added theorem RCLike.smul_re
added theorem RCLike.star_def
added theorem RCLike.sub_conj
added theorem RCLike.toOrderedSMul
added theorem RCLike.zero_re'
deleted theorem IsROrC.conjCLE_norm
deleted theorem IsROrC.ofRealCLM_norm
deleted theorem IsROrC.reCLM_norm
modified theorem Polynomial.aeval_ofReal
added theorem RCLike.conjCLE_norm
added theorem RCLike.ofRealCLM_norm
added theorem RCLike.reCLM_norm
modified theorem MeasureTheory.Integrable.im
modified theorem MeasureTheory.Integrable.re
modified theorem MeasureTheory.Memℒp.im
modified theorem MeasureTheory.Memℒp.re
deleted theorem AEMeasurable.im
deleted theorem AEMeasurable.re
deleted theorem IsROrC.measurable_im
deleted theorem IsROrC.measurable_ofReal
deleted theorem IsROrC.measurable_re
deleted theorem Measurable.im
deleted theorem Measurable.re
deleted theorem aemeasurable_of_re_im
deleted theorem measurable_of_re_im
added theorem AEMeasurable.im
added theorem AEMeasurable.re
added theorem Measurable.im
added theorem Measurable.re
added theorem RCLike.measurable_im
added theorem RCLike.measurable_re
added theorem aemeasurable_of_re_im
added theorem measurable_of_re_im
modified theorem MeasureTheory.integral_div
modified theorem integral_smul_const
modified theorem torusIntegral_smul