Commit 2024-05-05 02:43 26918687

View on Github →

feat: lemmas about Sigma.curry (#12474) This provides:

  • Basic simp lemmas for Equiv.piCurry
  • Algebraic lemmas for Sigma.curry and Sigma.uncurry
  • A LinearEquiv version of Equiv.piCurry
  • A lemma about Sigma.curry and Pi.mulSingle The change from Sort _ to Type* is a no-op, the _ was inferred as _ + 1.

Estimated changes

added theorem Sigma.curry_inv
added theorem Sigma.curry_mul
added theorem Sigma.curry_mulSingle
added theorem Sigma.curry_one
added theorem Sigma.uncurry_inv
added theorem Sigma.uncurry_mul
added theorem Sigma.uncurry_one
added theorem Sigma.curry_update
modified def Equiv.piCurry
added theorem Equiv.piCurry_apply