Theorem QuaternionAlgebra.coe_symm_addEquivTuple

Modification history

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