Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-24 11:52 d90149e9

View on Github →

feat(algebra/quaternion): add quaternion.im for the skew-adjoint part (#18456) As requested by @YaelDillies, as prework for #18349 where I need to split the quaternion into real and imaginary parts. Only one marginally interesting lemma is included, im_sq which says q.im^2 = -norm_sq q.im

Estimated changes

added theorem quaternion.add_im
added theorem quaternion.coe_im
added theorem quaternion.conj_im
added def quaternion.im
added theorem quaternion.im_conj
added theorem quaternion.im_idem
added theorem quaternion.im_im_i
added theorem quaternion.im_im_j
added theorem quaternion.im_im_k
added theorem quaternion.im_re
added theorem quaternion.im_sq
added theorem quaternion.int_cast_im
added theorem quaternion.nat_cast_im
added theorem quaternion.neg_im
added theorem quaternion.one_im
added theorem quaternion.rat_cast_im
added theorem quaternion.re_add_im
added theorem quaternion.smul_im
added theorem quaternion.sub_im
added theorem quaternion.sub_self_im
added theorem quaternion.sub_self_re
added theorem quaternion.zero_im
modified theorem quaternion_algebra.coe_im_i
modified theorem quaternion_algebra.coe_im_j
modified theorem quaternion_algebra.coe_im_k
modified theorem quaternion_algebra.coe_re