Theorems · Theorem
Function.FromTypes.uncurry_two_eq_uncurry
∀ (p : Fin 2 → Type u) (τ : Type u) (f : Function.FromTypes p τ), f.uncurry = Function.uncurry f ∘ ⇑(piFinTwoEquiv p)
- Defined in
- Mathlib.Data.Fin.Tuple.Curry
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement · cited by 8,337
- Matrix.vecTailstatement · cited by 39
- Matrix.vecHeadstatement · cited by 34
- Function.FromTypesstatement and proof · cited by 29
- piFinTwoEquivstatement · cited by 19
- Function.FromTypes.uncurrystatement · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- Function.OfArity.uncurry_two_eq_uncurryproof · cited by 0