mathlib3
e35d9760 - chore(algebra/quaternion): add `smul_mk` (#8126)

Commit

4 years ago

chore(algebra/quaternion): add `smul_mk` (#8126) This follows the pattern set by `mk_mul_mk` and `mk_add_mk`.

Author

eric-wieser

Parents