Documentation Verification Report

Curry

📁 Source: Mathlib/Data/Fin/Tuple/Curry.lean

Statistics

Metric	Count
Definitions `curry`, `curryEquiv`, `uncurry`, `curry`, `curryEquiv`, `uncurry`	6
Theorems `curryEquiv_apply`, `curryEquiv_symm_apply`, `curry_apply_cons`, `curry_apply_succ`, `curry_two_eq_curry`, `curry_uncurry`, `uncurry_apply_cons`, `uncurry_apply_succ`, `uncurry_curry`, `uncurry_two_eq_uncurry`, `curryEquiv_apply`, `curryEquiv_symm_apply`, `curry_two_eq_curry`, `curry_uncurry`, `uncurry_curry`, `uncurry_two_eq_uncurry`	16
Total	22

Function.FromTypes

Definitions

Name	Category	Theorems
`curry` 📖	CompOp	7 math math: `curry_two_eq_curry`, `curry_apply_succ`, `uncurry_curry`, `curry_uncurry`, `Function.OfArity.curryEquiv_apply`, `curryEquiv_apply`, `curry_apply_cons`
`curryEquiv` 📖	CompOp	2 math math: `curryEquiv_symm_apply`, `curryEquiv_apply`
`uncurry` 📖	CompOp	7 math math: `uncurry_apply_cons`, `Function.OfArity.curryEquiv_symm_apply`, `uncurry_apply_succ`, `curryEquiv_symm_apply`, `uncurry_two_eq_uncurry`, `uncurry_curry`, `curry_uncurry`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curryEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Function.FromTypes` `EquivLike.toFunLike` `Equiv.instEquivLike` `curryEquiv` `curry`	—	—
`curryEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Function.FromTypes` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `curryEquiv` `uncurry`	—	—
`curry_apply_cons` 📖	mathematical	—	`curry` `Matrix.vecCons` `Function.dcomp` `Fin.cons`	—	—
`curry_apply_succ` 📖	mathematical	—	`curry` `Fin.cons`	—	—
`curry_two_eq_curry` 📖	mathematical	—	`curry` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `piFinTwoEquiv`	—	—
`curry_uncurry` 📖	mathematical	—	`curry` `uncurry`	—	—
`uncurry_apply_cons` 📖	mathematical	—	`uncurry` `Matrix.vecCons` `Fin.cons`	—	—
`uncurry_apply_succ` 📖	mathematical	—	`uncurry` `Matrix.vecTail` `Fin.tail`	—	—
`uncurry_curry` 📖	mathematical	—	`uncurry` `curry`	—	`Fin.isEmpty'` `Unique.instSubsingleton` `Fin.cons_self_tail`
`uncurry_two_eq_uncurry` 📖	mathematical	—	`uncurry` `Matrix.vecHead` `Matrix.vecTail` `Function.FromTypes` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `piFinTwoEquiv`	—	—

Function.OfArity

Definitions

Name	Category	Theorems
`curry` 📖	CompOp	3 math math: `curry_uncurry`, `uncurry_curry`, `curry_two_eq_curry`
`curryEquiv` 📖	CompOp	2 math math: `curryEquiv_symm_apply`, `curryEquiv_apply`
`uncurry` 📖	CompOp	3 math math: `curry_uncurry`, `uncurry_curry`, `uncurry_two_eq_uncurry`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curryEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Function.OfArity` `EquivLike.toFunLike` `Equiv.instEquivLike` `curryEquiv` `Function.FromTypes.curry`	—	—
`curryEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Function.OfArity` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `curryEquiv` `Function.FromTypes.uncurry`	—	—
`curry_two_eq_curry` 📖	mathematical	—	`curry` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finTwoArrowEquiv`	—	`Function.FromTypes.curry_two_eq_curry`
`curry_uncurry` 📖	mathematical	—	`curry` `uncurry`	—	`Function.FromTypes.curry_uncurry`
`uncurry_curry` 📖	mathematical	—	`uncurry` `curry`	—	`Function.FromTypes.uncurry_curry`
`uncurry_two_eq_uncurry` 📖	mathematical	—	`uncurry` `Matrix.vecHead` `Matrix.vecTail` `Function.FromTypes` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finTwoArrowEquiv`	—	`Function.FromTypes.uncurry_two_eq_uncurry`

---

← Back to Index