Commit 2026-09-01 13:19 c3be5ef0

refactor: Quaternion as abbrev (#43078)

• Mark Quaternion as an abbrev. Cf. #mathlib4 > Transparency problem with quaternions @ 💬 and this comment.
• The instances for Quaternion that used to be proved by inferInstanceAs are removed.
• Remove five set_options as a consequence.
• Move normSq_ratCast so that it loses the assumptions [LinearOrder R] [IsStrictOrderedRing R].