mathlib3

d3e3adc9 - chore(algebra/quaternion): missing trivial lemmas (#18413)

chore(algebra/quaternion): missing trivial lemmas (#18413) A mixture of trivial algebraic results and trivial topological ones. This also changes the `rat.cast` instance on quaternions to be slightly nicer.