Theorem QuaternionAlgebra.hom_ext

Modification history

2025-01-24 00:30
Mathlib/Algebra/QuaternionBasis.lean
chore(Mathlib/Algebra/Quaternion): Generalize Quaternion Algebra (#20657)
Modified QuaternionAlgebra.hom_extView on Github →
2024-01-05 11:32
Mathlib/Algebra/QuaternionBasis.lean
feat(Algebra/QuaternionBasis): extensionality for algebra morphisms from quaternions (#9441) …
Added QuaternionAlgebra.hom_extView on Github →