Commit 2023-06-24 12:17 8b9210ba

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.Fold (#5406)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean

added def CliffordAlgebra.foldl

added theorem CliffordAlgebra.foldl_algebraMap

added theorem CliffordAlgebra.foldl_mul

added theorem CliffordAlgebra.foldl_one

added theorem CliffordAlgebra.foldl_prod_map_ι

added theorem CliffordAlgebra.foldl_reverse

added theorem CliffordAlgebra.foldl_ι

added def CliffordAlgebra.foldr'

added def CliffordAlgebra.foldr'Aux

added theorem CliffordAlgebra.foldr'Aux_apply_apply

added theorem CliffordAlgebra.foldr'Aux_foldr'Aux

added theorem CliffordAlgebra.foldr'_algebraMap

added theorem CliffordAlgebra.foldr'_ι

added theorem CliffordAlgebra.foldr'_ι_mul

added def CliffordAlgebra.foldr

added theorem CliffordAlgebra.foldr_algebraMap

added theorem CliffordAlgebra.foldr_mul

added theorem CliffordAlgebra.foldr_one

added theorem CliffordAlgebra.foldr_prod_map_ι

added theorem CliffordAlgebra.foldr_reverse

added theorem CliffordAlgebra.foldr_ι

added theorem CliffordAlgebra.left_induction

added theorem CliffordAlgebra.right_induction