Commit 2020-10-01 14:27 13e9cc4a

View on Github →

feat(linear_algebra/exterior_algebra): Add an exterior algebra (#4297) This adds the basic exterior algebra definitions using a very similar approach to universal_enveloping_algebra. It's based off the exterior_algebra branch, dropping the wedge stuff for now as development in multilinear maps is happening elsewhere.

Estimated changes

Created src/linear_algebra/exterior_algebra.lean

added theorem exterior_algebra.comp_ι_square_zero

added theorem exterior_algebra.hom_ext

added def exterior_algebra.lift

added theorem exterior_algebra.lift_comp_ι

added theorem exterior_algebra.lift_unique

added theorem exterior_algebra.lift_ι_apply

added inductive exterior_algebra.rel

added def exterior_algebra.ι

added theorem exterior_algebra.ι_comp_lift

added theorem exterior_algebra.ι_square_zero

added def exterior_algebra