mathlib

d90149e9 - feat(algebra/quaternion): add `quaternion.im` for the skew-adjoint part (#18456)

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`