Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-29 09:17 cf7a7252

View on Github →

refactor(algebra/quaternion): remove quaternion.conj (#18803) Instead we use star directly. We keep only the lemmas that refer to quaternion-specific operators, as the rest are already covered by the star API. In practice, this is mostly the lemmas about the real and imaginary parts of quaternions. The commute_self_conj lemma has been replaced by a is_star_normal instance.

Estimated changes

deleted theorem quaternion.coe_conj_ae
added theorem quaternion.coe_star_ae
deleted def quaternion.conj
deleted theorem quaternion.conj_add
deleted theorem quaternion.conj_add_self'
deleted theorem quaternion.conj_add_self
deleted def quaternion.conj_ae
deleted theorem quaternion.conj_coe
deleted theorem quaternion.conj_conj
deleted theorem quaternion.conj_conj_mul
deleted theorem quaternion.conj_eq_neg
deleted theorem quaternion.conj_eq_self
deleted theorem quaternion.conj_im
deleted theorem quaternion.conj_im_i
deleted theorem quaternion.conj_im_j
deleted theorem quaternion.conj_im_k
deleted theorem quaternion.conj_int_cast
deleted theorem quaternion.conj_inv
deleted theorem quaternion.conj_mul
deleted theorem quaternion.conj_mul_conj
deleted theorem quaternion.conj_mul_self
deleted theorem quaternion.conj_nat_cast
deleted theorem quaternion.conj_neg
deleted theorem quaternion.conj_one
deleted theorem quaternion.conj_pow
deleted theorem quaternion.conj_rat_cast
deleted theorem quaternion.conj_re
deleted theorem quaternion.conj_smul
deleted theorem quaternion.conj_sub
deleted theorem quaternion.conj_zero
deleted theorem quaternion.conj_zpow
deleted theorem quaternion.im_conj
added theorem quaternion.im_star
modified theorem quaternion.norm_sq_add
deleted theorem quaternion.norm_sq_conj
modified theorem quaternion.norm_sq_def
deleted theorem quaternion.self_add_conj'
deleted theorem quaternion.self_add_conj
deleted theorem quaternion.self_mul_conj
added theorem quaternion.star_coe
added theorem quaternion.star_eq_neg
added theorem quaternion.star_im
added theorem quaternion.star_im_i
added theorem quaternion.star_im_j
added theorem quaternion.star_im_k
added theorem quaternion.star_re
added theorem quaternion.star_smul
deleted theorem quaternion.conj_exp
modified theorem quaternion.inner_def
deleted theorem quaternion.nnnorm_conj
added theorem quaternion.nnnorm_star
deleted theorem quaternion.norm_conj
added theorem quaternion.norm_star