Commit 2023-06-23 04:14 4a17605f

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.Grading (#5349) This runs into some annoying problems with https://github.com/leanprover/lean4/issues/1926 which makes working with the dependent types much worse than it was in Lean 3.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

added theorem CliffordAlgebra.GradedAlgebra.lift_ι_eq

added theorem CliffordAlgebra.GradedAlgebra.ι_apply

added def CliffordAlgebra.evenOdd

added theorem CliffordAlgebra.evenOdd_induction

added theorem CliffordAlgebra.evenOdd_isCompl

added theorem CliffordAlgebra.evenOdd_mul_le

added theorem CliffordAlgebra.even_induction

added theorem CliffordAlgebra.iSup_ι_range_eq_top

added theorem CliffordAlgebra.odd_induction

added theorem CliffordAlgebra.one_le_evenOdd_zero

added theorem CliffordAlgebra.range_ι_le_evenOdd_one

added theorem CliffordAlgebra.ι_mem_evenOdd_one

added theorem CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero