Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-25 07:57 07c83c81

View on Github →

feat(linear_algebra/clifford_algebra/of_alternating): extend alternating maps to the exterior algebra (#14803)

Estimated changes

Modified src/linear_algebra/exterior_algebra/basic.lean

Created src/linear_algebra/exterior_algebra/of_alternating.lean

added theorem exterior_algebra.lhom_ext

added def exterior_algebra.lift_alternating

added theorem exterior_algebra.lift_alternating_algebra_map

added theorem exterior_algebra.lift_alternating_apply_ι_multi

added theorem exterior_algebra.lift_alternating_comp

added theorem exterior_algebra.lift_alternating_comp_ι_multi

added def exterior_algebra.lift_alternating_equiv

added theorem exterior_algebra.lift_alternating_one

added theorem exterior_algebra.lift_alternating_ι

added theorem exterior_algebra.lift_alternating_ι_mul

added theorem exterior_algebra.lift_alternating_ι_multi