Commit 2023-06-22 04:55 96e68449

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.Basic (#4802)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

added inductive CliffordAlgebra.Rel

added theorem CliffordAlgebra.comp_ι_sq_scalar

added def CliffordAlgebra.equivOfIsometry

added theorem CliffordAlgebra.equivOfIsometry_refl

added theorem CliffordAlgebra.equivOfIsometry_symm

added theorem CliffordAlgebra.equivOfIsometry_trans

added theorem CliffordAlgebra.hom_ext

added theorem CliffordAlgebra.induction

added theorem CliffordAlgebra.invOf_ι

added theorem CliffordAlgebra.invOf_ι_mul_ι_mul_ι

added def CliffordAlgebra.invertibleιOfInvertible

added theorem CliffordAlgebra.isUnit_ι_of_isUnit

added def CliffordAlgebra.lift

added theorem CliffordAlgebra.lift_comp_ι

added theorem CliffordAlgebra.lift_unique

added theorem CliffordAlgebra.lift_ι_apply

added def CliffordAlgebra.map

added theorem CliffordAlgebra.map_apply_ι

added theorem CliffordAlgebra.map_comp_map

added theorem CliffordAlgebra.map_comp_ι

added theorem CliffordAlgebra.map_id

added def CliffordAlgebra.ι

added theorem CliffordAlgebra.ι_comp_lift

added theorem CliffordAlgebra.ι_mul_comm

added theorem CliffordAlgebra.ι_mul_ι_add_swap

added theorem CliffordAlgebra.ι_mul_ι_mul_invOf_ι

added theorem CliffordAlgebra.ι_mul_ι_mul_ι

added theorem CliffordAlgebra.ι_range_map_lift

added theorem CliffordAlgebra.ι_range_map_map

added theorem CliffordAlgebra.ι_sq_scalar

added def CliffordAlgebra

added def TensorAlgebra.toClifford

added theorem TensorAlgebra.toClifford_ι