Commit 2025-12-12 14:22 08b58866

View on Github →

refactor(Algebra/Quaternion): intermediate Module instance (#30678) This Module instance allows me to not ungeneralise the NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃] in #30563.

Estimated changes

Modified Mathlib/Algebra/Quaternion.lean

added def QuaternionAlgebra.addEquivProd

added def QuaternionAlgebra.addEquivTuple

added theorem QuaternionAlgebra.coe_addEquivProd

added theorem QuaternionAlgebra.coe_addEquivTuple

added theorem QuaternionAlgebra.coe_symm_addEquivProd

added theorem QuaternionAlgebra.coe_symm_addEquivTuple

modified def QuaternionAlgebra.linearEquivTuple