mathlib
4a8467a4 - feat(data/equiv/basic): equiv.curry (#7458)

Commit
4 years ago
feat(data/equiv/basic): equiv.curry (#7458) This renames `equiv.arrow_arrow_equiv_prod_arrow` to `(equiv.curry _ _ _).symm` to make it easier to find and match `function.curry`. * `cardinal.power_mul` is swapped, so that its name makes sense. * renames `linear_equiv.uncurry` to `linear_equiv.curry` and swaps sides Also add `@[simps]` to two equivs.
Author
Parents
Loading