Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-19 16:19 5dc8bc16

View on Github →

feat(linear_algebra/clifford_algebra/equivs): the equivalences preserve conjugation (#8739)

Estimated changes

Modified src/algebra/quaternion.lean

added theorem quaternion_algebra.conj_mk

Modified src/linear_algebra/clifford_algebra/equivs.lean

added def clifford_algebra_complex.of_complex

added theorem clifford_algebra_complex.of_complex_I

added theorem clifford_algebra_complex.of_complex_comp_to_complex

added theorem clifford_algebra_complex.of_complex_conj

added theorem clifford_algebra_complex.of_complex_to_complex

added theorem clifford_algebra_complex.reverse_apply

added theorem clifford_algebra_complex.reverse_eq_id

added theorem clifford_algebra_complex.to_complex_comp_of_complex

added theorem clifford_algebra_complex.to_complex_involute

added theorem clifford_algebra_complex.to_complex_of_complex

deleted theorem clifford_algebra_quaternion.of_quaternion_apply

added theorem clifford_algebra_quaternion.of_quaternion_conj

added theorem clifford_algebra_quaternion.of_quaternion_mk

added theorem clifford_algebra_quaternion.of_quaternion_to_quaternion

added theorem clifford_algebra_quaternion.to_quaternion_involute_reverse

added theorem clifford_algebra_quaternion.to_quaternion_of_quaternion

added theorem clifford_algebra_ring.involute_eq_id

added theorem clifford_algebra_ring.reverse_apply

added theorem clifford_algebra_ring.reverse_eq_id