Commit 2025-09-01 09:41 51d0ba3f

View on Github →

refactor: correct names of quaternion lemmas (#29190) This renames lemmas of the form (foo x).re to be called re_foo instead of foo_re, and similarly for imI, imJ, imK, and im, to match the naming guide. These are then all deprecated with the deprecation script. I did not attempt to deprecated the relocated simps lemmas. Some lemmas ended up exchanged and could not be deprecated, listed below: Moves:

  • Quaternion.im_star -> Quaternion.star_im
  • Quaternion.star_im-> Quaternion.im_star
  • QuaternionAlgebra.im_star -> QuaternionAlgebra.star_im
  • QuaternionAlgebra.star_im-> QuaternionAlgebra.im_star

Estimated changes

deleted theorem Quaternion.add_imI
deleted theorem Quaternion.add_imJ
deleted theorem Quaternion.add_imK
deleted theorem Quaternion.add_re
deleted theorem Quaternion.coe_im
deleted theorem Quaternion.coe_imI
deleted theorem Quaternion.coe_imJ
deleted theorem Quaternion.coe_imK
deleted theorem Quaternion.coe_re
added theorem Quaternion.imI_add
added theorem Quaternion.imI_coe
added theorem Quaternion.imI_im
added theorem Quaternion.imI_intCast
added theorem Quaternion.imI_mul
added theorem Quaternion.imI_natCast
added theorem Quaternion.imI_neg
added theorem Quaternion.imI_one
added theorem Quaternion.imI_ratCast
added theorem Quaternion.imI_smul
added theorem Quaternion.imI_star
added theorem Quaternion.imI_sub
added theorem Quaternion.imI_zero
added theorem Quaternion.imJ_add
added theorem Quaternion.imJ_coe
added theorem Quaternion.imJ_im
added theorem Quaternion.imJ_intCast
added theorem Quaternion.imJ_mul
added theorem Quaternion.imJ_natCast
added theorem Quaternion.imJ_neg
added theorem Quaternion.imJ_one
added theorem Quaternion.imJ_ratCast
added theorem Quaternion.imJ_smul
added theorem Quaternion.imJ_star
added theorem Quaternion.imJ_sub
added theorem Quaternion.imJ_zero
added theorem Quaternion.imK_add
added theorem Quaternion.imK_coe
added theorem Quaternion.imK_im
added theorem Quaternion.imK_intCast
added theorem Quaternion.imK_mul
added theorem Quaternion.imK_natCast
added theorem Quaternion.imK_neg
added theorem Quaternion.imK_one
added theorem Quaternion.imK_ratCast
added theorem Quaternion.imK_smul
added theorem Quaternion.imK_star
added theorem Quaternion.imK_sub
added theorem Quaternion.imK_zero
added theorem Quaternion.im_coe
deleted theorem Quaternion.im_imI
deleted theorem Quaternion.im_imJ
deleted theorem Quaternion.im_imK
added theorem Quaternion.im_intCast
added theorem Quaternion.im_natCast
added theorem Quaternion.im_one
added theorem Quaternion.im_ratCast
deleted theorem Quaternion.im_re
modified theorem Quaternion.im_star
added theorem Quaternion.im_zero
deleted theorem Quaternion.intCast_im
deleted theorem Quaternion.intCast_imI
deleted theorem Quaternion.intCast_imJ
deleted theorem Quaternion.intCast_imK
deleted theorem Quaternion.intCast_re
deleted theorem Quaternion.mul_imI
deleted theorem Quaternion.mul_imJ
deleted theorem Quaternion.mul_imK
deleted theorem Quaternion.mul_re
deleted theorem Quaternion.natCast_im
deleted theorem Quaternion.natCast_imI
deleted theorem Quaternion.natCast_imJ
deleted theorem Quaternion.natCast_imK
deleted theorem Quaternion.natCast_re
deleted theorem Quaternion.neg_imI
deleted theorem Quaternion.neg_imJ
deleted theorem Quaternion.neg_imK
deleted theorem Quaternion.neg_re
deleted theorem Quaternion.one_im
deleted theorem Quaternion.one_imI
deleted theorem Quaternion.one_imJ
deleted theorem Quaternion.one_imK
deleted theorem Quaternion.one_re
deleted theorem Quaternion.ratCast_im
deleted theorem Quaternion.ratCast_imI
deleted theorem Quaternion.ratCast_imJ
deleted theorem Quaternion.ratCast_imK
deleted theorem Quaternion.ratCast_re
added theorem Quaternion.re_add
added theorem Quaternion.re_coe
added theorem Quaternion.re_im
added theorem Quaternion.re_intCast
added theorem Quaternion.re_mul
added theorem Quaternion.re_natCast
added theorem Quaternion.re_neg
added theorem Quaternion.re_one
added theorem Quaternion.re_ratCast
added theorem Quaternion.re_smul
added theorem Quaternion.re_star
added theorem Quaternion.re_sub
added theorem Quaternion.re_zero
deleted theorem Quaternion.smul_imI
deleted theorem Quaternion.smul_imJ
deleted theorem Quaternion.smul_imK
deleted theorem Quaternion.smul_re
modified theorem Quaternion.star_im
deleted theorem Quaternion.star_imI
deleted theorem Quaternion.star_imJ
deleted theorem Quaternion.star_imK
deleted theorem Quaternion.star_re
deleted theorem Quaternion.sub_imI
deleted theorem Quaternion.sub_imJ
deleted theorem Quaternion.sub_imK
deleted theorem Quaternion.sub_re
deleted theorem Quaternion.zero_im
deleted theorem Quaternion.zero_imI
deleted theorem Quaternion.zero_imJ
deleted theorem Quaternion.zero_imK
deleted theorem Quaternion.zero_re
deleted theorem QuaternionAlgebra.add_im
deleted theorem QuaternionAlgebra.coe_im
deleted theorem QuaternionAlgebra.coe_imI
deleted theorem QuaternionAlgebra.coe_imJ
deleted theorem QuaternionAlgebra.coe_imK
deleted theorem QuaternionAlgebra.coe_re
deleted theorem QuaternionAlgebra.im_imI
deleted theorem QuaternionAlgebra.im_imJ
deleted theorem QuaternionAlgebra.im_imK
deleted theorem QuaternionAlgebra.im_re
deleted theorem QuaternionAlgebra.neg_im
deleted theorem QuaternionAlgebra.one_im
deleted theorem QuaternionAlgebra.smul_im
deleted theorem QuaternionAlgebra.sub_im
deleted theorem QuaternionAlgebra.zero_im
deleted theorem Quaternion.coeComplex_imI
deleted theorem Quaternion.coeComplex_imJ
deleted theorem Quaternion.coeComplex_imK
deleted theorem Quaternion.coeComplex_re