Commit 2024-01-05 11:32 0c2c47a2

View on Github →

feat(Algebra/QuaternionBasis): extensionality for algebra morphisms from quaternions (#9441) This result was basically already here, this just registers it with ext.

Estimated changes

Modified Mathlib/Algebra/QuaternionBasis.lean

added theorem Quaternion.hom_ext

added theorem QuaternionAlgebra.hom_ext

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean