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.

Estimated changes

modified theorem Quaternion.one_im
modified theorem Quaternion.one_imI
modified theorem Quaternion.one_imJ
modified theorem Quaternion.one_imK
modified theorem Quaternion.one_re
modified theorem Quaternion.zero_im
modified theorem Quaternion.zero_imI
modified theorem Quaternion.zero_imJ
modified theorem Quaternion.zero_imK
modified theorem Quaternion.zero_re
modified theorem QuaternionAlgebra.one_im
modified theorem QuaternionAlgebra.one_imI
modified theorem QuaternionAlgebra.one_imJ
modified theorem QuaternionAlgebra.one_imK
modified theorem QuaternionAlgebra.one_re
modified theorem QuaternionAlgebra.zero_im
modified theorem QuaternionAlgebra.zero_imI
modified theorem QuaternionAlgebra.zero_imJ
modified theorem QuaternionAlgebra.zero_imK
modified theorem QuaternionAlgebra.zero_re