mathlib3

dc7ac07a - chore(algebra/star/basic): generalize quaternion lemmas (#18802)

chore(algebra/star/basic): generalize quaternion lemmas (#18802) We already had most of these lemmas specialized to quaternions; this generalizes them to any star ring. We should consider replacing `quaternion.conj` with `star` in future.