Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-14 14:46 442ef226

View on Github →

feat(linear_algebra/clifford_algebra): Add a definition derived from exterior_algebra.lean (#4430)

Estimated changes

Created src/linear_algebra/clifford_algebra.lean

added def clifford_algebra.as_exterior

added theorem clifford_algebra.comp_ι_square_scalar

added theorem clifford_algebra.hom_ext

added def clifford_algebra.lift

added theorem clifford_algebra.lift_comp_ι

added theorem clifford_algebra.lift_unique

added theorem clifford_algebra.lift_ι_apply

added inductive clifford_algebra.rel

added def clifford_algebra.ι

added theorem clifford_algebra.ι_comp_lift

added theorem clifford_algebra.ι_square_scalar

added def clifford_algebra

Modified src/linear_algebra/exterior_algebra.lean