Commit 2023-07-06 17:06 7f54ac4a

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.Contraction (#5467)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

added theorem CliffordAlgebra.changeForm.add_proof

added theorem CliffordAlgebra.changeForm.associated_neg_proof

added theorem CliffordAlgebra.changeForm.neg_proof

added theorem CliffordAlgebra.changeForm.zero_proof

added def CliffordAlgebra.changeForm

added def CliffordAlgebra.changeFormAux

added theorem CliffordAlgebra.changeFormAux_changeFormAux

added def CliffordAlgebra.changeFormEquiv

added theorem CliffordAlgebra.changeFormEquiv_symm

added theorem CliffordAlgebra.changeForm_algebraMap

added theorem CliffordAlgebra.changeForm_changeForm

added theorem CliffordAlgebra.changeForm_comp_changeForm

added theorem CliffordAlgebra.changeForm_contractLeft

added theorem CliffordAlgebra.changeForm_one

added theorem CliffordAlgebra.changeForm_self

added theorem CliffordAlgebra.changeForm_self_apply

added theorem CliffordAlgebra.changeForm_ι

added theorem CliffordAlgebra.changeForm_ι_mul

added theorem CliffordAlgebra.changeForm_ι_mul_ι

added def CliffordAlgebra.contractLeft

added def CliffordAlgebra.contractLeftAux

added theorem CliffordAlgebra.contractLeftAux_contractLeftAux

added theorem CliffordAlgebra.contractLeft_algebraMap

added theorem CliffordAlgebra.contractLeft_algebraMap_mul

added theorem CliffordAlgebra.contractLeft_comm

added theorem CliffordAlgebra.contractLeft_contractLeft

added theorem CliffordAlgebra.contractLeft_mul_algebraMap

added theorem CliffordAlgebra.contractLeft_one

added theorem CliffordAlgebra.contractLeft_ι

added theorem CliffordAlgebra.contractLeft_ι_mul

added def CliffordAlgebra.contractRight

added theorem CliffordAlgebra.contractRight_algebraMap

added theorem CliffordAlgebra.contractRight_algebraMap_mul

added theorem CliffordAlgebra.contractRight_comm

added theorem CliffordAlgebra.contractRight_contractRight

added theorem CliffordAlgebra.contractRight_eq

added theorem CliffordAlgebra.contractRight_mul_algebraMap

added theorem CliffordAlgebra.contractRight_mul_ι

added theorem CliffordAlgebra.contractRight_one

added theorem CliffordAlgebra.contractRight_ι

added def CliffordAlgebra.equivExterior