Commit 2023-05-22 17:42 75a6e216

View on Github →

feat: port Algebra.QuaternionBasis (#4199)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/QuaternionBasis.lean

added def QuaternionAlgebra.Basis.compHom

added theorem QuaternionAlgebra.Basis.i_mul_k

added theorem QuaternionAlgebra.Basis.j_mul_k

added theorem QuaternionAlgebra.Basis.k_mul_i

added theorem QuaternionAlgebra.Basis.k_mul_j

added theorem QuaternionAlgebra.Basis.k_mul_k

added def QuaternionAlgebra.Basis.lift

added def QuaternionAlgebra.Basis.liftHom

added theorem QuaternionAlgebra.Basis.lift_add

added theorem QuaternionAlgebra.Basis.lift_mul

added theorem QuaternionAlgebra.Basis.lift_one

added theorem QuaternionAlgebra.Basis.lift_smul

added theorem QuaternionAlgebra.Basis.lift_zero

added structure QuaternionAlgebra.Basis

added def QuaternionAlgebra.lift