Theorem QuaternionAlgebra.coe_symm_addEquivProd

Modification history

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