Commit 2023-06-23 08:17 7b95035d

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.Star (#5405)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean

added theorem CliffordAlgebra.star_algebraMap

added theorem CliffordAlgebra.star_def'

added theorem CliffordAlgebra.star_def

added theorem CliffordAlgebra.star_smul

added theorem CliffordAlgebra.star_ι