Def QuaternionAlgebra.addEquivProd

Modification history

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