Theorem Quaternion.hom_ext

Modification history

2024-01-05 11:32
Mathlib/Algebra/QuaternionBasis.lean
feat(Algebra/QuaternionBasis): extensionality for algebra morphisms from quaternions (#9441) …
Added Quaternion.hom_extView on Github →