Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exterior_algebra.lhom_ext

Modification history

2022-06-25 07:57
src/linear_algebra/exterior_algebra/of_alternating.lean
feat(linear_algebra/clifford_algebra/of_alternating): extend alternating maps to the exterior algebra (#14803)
Added exterior_algebra.lhom_extView on Github →