Commit 2023-06-29 18:19 eef7daf0

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.Even (#5408)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean

added def CliffordAlgebra.EvenHom.compr₂

added structure CliffordAlgebra.EvenHom

added theorem CliffordAlgebra.even.algHom_ext

added def CliffordAlgebra.even.lift.aux

added theorem CliffordAlgebra.even.lift.aux_algebraMap

added theorem CliffordAlgebra.even.lift.aux_mul

added theorem CliffordAlgebra.even.lift.aux_one

added theorem CliffordAlgebra.even.lift.aux_ι

added def CliffordAlgebra.even.lift

added theorem CliffordAlgebra.even.lift_ι

added def CliffordAlgebra.even

added theorem CliffordAlgebra.even_toSubmodule