mathlib

3b8cfdc9 - feat(linear_algebra/{exterior,tensor,free}_algebra): provide left-inverses for `algebra_map` and `ι` (#5722)

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`.