Commit 2025-02-14 20:32 ff071dfa
View on Github →chore(Algebra.Quaternion): scope simp theorems with weak keys (#21029)
The discrimination keys of these do not reference QuaternionAlgebra
so can apply broadly with simp
. There is already essential notation scoped to this namespace so open scoped QuaternionAlgebra
should not burden the user any more than it does currently.