Mathlib Changelog
Changelog
About
Github
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