Commit 2023-09-08 14:39 686be169

View on Github →

refactor(LinearAlgebra/CliffordAlgebra/Conjugation): expose implementation details of 'reverse' (#6783) Having the fully-bundled AlgHom (to MulOpposite) is occasionally useful for building larger AlgHoms, especially if the MulOpposite can be cancelled out later.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem AlgEquiv.toLinearMap_ofAlgHom

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean

added theorem CliffordAlgebra.op_reverse

modified theorem CliffordAlgebra.reverse.map_one

added def CliffordAlgebra.reverseOp

added def CliffordAlgebra.reverseOpEquiv

added theorem CliffordAlgebra.reverseOpEquiv_opComm

added theorem CliffordAlgebra.reverseOp_ι

added theorem CliffordAlgebra.unop_reverseOp