Commit 2023-09-16 17:31 eec55af4

View on Github →

feat: base change of Clifford algebras (#6778) The main result here is CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q; that is, the A ⊗[R] can be moved from _ : QuadraticForm A (A ⊗[R] _) to the outside and vice versa.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

added def CliffordAlgebra.equivBaseChange

added def CliffordAlgebra.ofBaseChange

added def CliffordAlgebra.ofBaseChangeAux

added theorem CliffordAlgebra.ofBaseChangeAux_ι

added theorem CliffordAlgebra.ofBaseChange_comp_toBaseChange

added theorem CliffordAlgebra.ofBaseChange_tmul_one

added theorem CliffordAlgebra.ofBaseChange_tmul_ι

added theorem CliffordAlgebra.ofBaseChange_toBaseChange

added def CliffordAlgebra.toBaseChange

added theorem CliffordAlgebra.toBaseChange_comp_involute

added theorem CliffordAlgebra.toBaseChange_comp_ofBaseChange

added theorem CliffordAlgebra.toBaseChange_comp_reverseOp

added theorem CliffordAlgebra.toBaseChange_involute

added theorem CliffordAlgebra.toBaseChange_ofBaseChange

added theorem CliffordAlgebra.toBaseChange_reverse

added theorem CliffordAlgebra.toBaseChange_ι

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

added theorem CliffordAlgebra.forall_mul_self_eq_iff

added theorem CliffordAlgebra.mul_add_swap_eq_polar_of_forall_mul_self_eq