Commit 2023-08-25 10:49 ed9d5590

View on Github →

chore(LinearAlgebra/CliffordAlgebra): remove Q := Q (#6780) The removal of a FunLike instance for Module.Dual made these unnecessary.

Estimated changes

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean

modified theorem CliffordAlgebra.reverse.map_one

modified theorem CliffordAlgebra.reverse_reverse

modified theorem CliffordAlgebra.reverse_ι

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean

modified theorem CliffordAlgebra.star_def'

modified theorem CliffordAlgebra.star_def