Commit 2023-10-14 13:46 f4abbaa7

View on Github →

feat: some basic quaternion facts (#7119)

Estimated changes

Modified Mathlib/Algebra/Quaternion.lean

added theorem Quaternion.algebraMap_injective

added theorem QuaternionAlgebra.algebraMap_injective

added def QuaternionAlgebra.swapEquiv