mathlib3

bd6b98b2 - feat(linear_algebra/alternating): add more compositional API (#14802)

feat(linear_algebra/alternating): add more compositional API (#14802) These will be helpful in relating `alternating_map`s to the `exterior_algebra`. This adds: * `alternating_map.curry_left` * `alternating_map.const_linear_equiv_of_is_empty` * `alternating_map.dom_dom_congr`