Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 07:53 41f7b5ba

View on Github →

feat(linear_algebra/clifford_algebra/equivs): there is a clifford algebra isomorphic to every quaternion algebra (#8670) The proofs are not particularly fast here unfortunately.

Estimated changes

Modified src/linear_algebra/clifford_algebra/basic.lean

added theorem clifford_algebra.ι_mul_ι_add_swap

Modified src/linear_algebra/clifford_algebra/equivs.lean

modified theorem clifford_algebra_complex.to_complex_ι

added def clifford_algebra_quaternion.Q

added theorem clifford_algebra_quaternion.Q_apply

added def clifford_algebra_quaternion.of_quaternion

added theorem clifford_algebra_quaternion.of_quaternion_apply

added theorem clifford_algebra_quaternion.of_quaternion_comp_to_quaternion

added def clifford_algebra_quaternion.quaternion_basis

added def clifford_algebra_quaternion.to_quaternion

added theorem clifford_algebra_quaternion.to_quaternion_comp_of_quaternion

added theorem clifford_algebra_quaternion.to_quaternion_ι