Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-14 19:06 3b8cfdc9

View on Github →

feat(linear_algebra/{exterior,tensor,free}_algebra): provide left-inverses for algebra_map and ι (#5722) The strategy used for algebra_map here can't be used on clifford_algebra as the zero map does not satisfy f m * f m = Q m.

Estimated changes