Theorem QuaternionAlgebra.coe_addEquivProd

Modification history

2025-12-12 14:22
Mathlib/Algebra/Quaternion.lean
refactor(Algebra/Quaternion): intermediate `Module` instance (#30678) …
Added QuaternionAlgebra.coe_addEquivProdView on Github →