Commit 2022-08-10 13:06 4d66277c

View on Github →

feat(linear_algebra/clifford_algebra/star): add a possibly-non-canonical star structure (#15866) See the module docstring for a discussion of non-canonicity.

Estimated changes

Modified src/linear_algebra/clifford_algebra/equivs.lean

deleted theorem clifford_algebra_quaternion.to_quaternion_involute_reverse

added theorem clifford_algebra_quaternion.to_quaternion_star

Created src/linear_algebra/clifford_algebra/star.lean

added theorem clifford_algebra.star_algebra_map

added theorem clifford_algebra.star_def'

added theorem clifford_algebra.star_def

added theorem clifford_algebra.star_smul

added theorem clifford_algebra.star_ι