Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-10 07:36 4a8467a4

View on Github →

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.

Estimated changes

added def equiv.curry
modified def equiv.prod_punit
modified def equiv.punit_prod
added theorem linear_equiv.coe_curry
deleted theorem linear_equiv.coe_uncurry
modified theorem cardinal.power_mul