Commit 2023-02-13 19:19 48085f14

View on Github →

chore(algebra/quaternion): generalize the algebra instance (#18382) To prevent this generalization forming diamonds, we have to now populate the nsmul, zsmul, and qsmul fields. I use this in another PR to talk about the R algebra structure of quaternion (dual_number R). Even without that motivation, this change means that the existing smul lemmas now apply to nsmul, zsmul, and rat_smul where previously they did not.

Estimated changes

Modified src/algebra/quaternion.lean

added theorem quaternion.coe_smul

modified theorem quaternion.conj_smul

modified theorem quaternion.smul_im_i

modified theorem quaternion.smul_im_j

modified theorem quaternion.smul_im_k

modified theorem quaternion.smul_re

added theorem quaternion_algebra.coe_smul

modified theorem quaternion_algebra.conj_smul

modified theorem quaternion_algebra.smul_im_i

modified theorem quaternion_algebra.smul_im_j

modified theorem quaternion_algebra.smul_im_k

modified theorem quaternion_algebra.smul_re

Modified src/analysis/quaternion.lean