Curry

📁 Source: Mathlib/LinearAlgebra/Multilinear/Curry.lean

Statistics

Metric	Count
Definitions uncurryLeft, uncurryMid, curryFinFinset, curryLeft, curryMid, curryMidLinearEquiv, curryRight, currySum, currySumEquiv, uncurryRight, uncurrySum, multilinearCurryLeftEquiv, multilinearCurryRightEquiv	13
Theorems curryMid_uncurryMid, curry_uncurryLeft, uncurryLeft_apply, uncurryMid_apply, coe_currySumEquiv, coe_currySumEquiv_symm, curryFinFinset_apply, curryFinFinset_apply_const, curryFinFinset_symm_apply, curryFinFinset_symm_apply_const, curryFinFinset_symm_apply_piecewise_const, curryLeft_apply, curryMidLinearEquiv_apply, curryMidLinearEquiv_symm_apply, curryMid_apply_apply, curryRight_apply, currySumEquiv_apply, currySumEquiv_symm_apply, currySum_add, currySum_apply, currySum_apply', currySum_smul, currySum_uncurrySum, curry_uncurryRight, uncurryMid_curryMid, uncurryRight_apply, uncurrySum_add, uncurrySum_apply, uncurrySum_currySum, uncurrySum_smul, uncurry_curryLeft, uncurry_curryRight, multilinearCurryLeftEquiv_apply, multilinearCurryLeftEquiv_symm_apply	34
Total	47

LinearMap

Definitions

Name	Category	Theorems
uncurryLeft 📖	CompOp	4 math math: MultilinearMap.uncurry_curryLeft, multilinearCurryLeftEquiv_symm_apply, curry_uncurryLeft, uncurryLeft_apply
uncurryMid 📖	CompOp	4 math math: curryMid_uncurryMid, MultilinearMap.uncurryMid_curryMid, uncurryMid_apply, MultilinearMap.curryMidLinearEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curryMid_uncurryMid 📖	mathematical	—	MultilinearMap.curryMid uncurryMid	—	smulCommClass_self ext MultilinearMap.ext Fin.insertNth_apply_same Fin.removeNth_insertNth
curry_uncurryLeft 📖	mathematical	—	MultilinearMap.curryLeft uncurryLeft	—	smulCommClass_self
uncurryLeft_apply 📖	mathematical	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring MultilinearMap.instFunLikeForall uncurryLeft LinearMap RingHom.id Semiring.toNonAssocSemiring MultilinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike Fin.tail	—	smulCommClass_self
uncurryMid_apply 📖	mathematical	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring MultilinearMap.instFunLikeForall uncurryMid Fin.succAbove LinearMap RingHom.id Semiring.toNonAssocSemiring MultilinearMap.addCommMonoid MultilinearMap.instModule instFunLike Fin.removeNth	—	smulCommClass_self

MultilinearMap

Definitions

Name	Category	Theorems
curryFinFinset 📖	CompOp	5 math math: curryFinFinset_apply, curryFinFinset_symm_apply_piecewise_const, curryFinFinset_apply_const, curryFinFinset_symm_apply_const, curryFinFinset_symm_apply
curryLeft 📖	CompOp	5 math math: AlternatingMap.curryLeft_apply_toMultilinearMap, uncurry_curryLeft, curryLeft_apply, multilinearCurryLeftEquiv_apply, LinearMap.curry_uncurryLeft
curryMid 📖	CompOp	4 math math: LinearMap.curryMid_uncurryMid, uncurryMid_curryMid, curryMid_apply_apply, curryMidLinearEquiv_apply
curryMidLinearEquiv 📖	CompOp	2 math math: curryMidLinearEquiv_apply, curryMidLinearEquiv_symm_apply
curryRight 📖	CompOp	3 math math: curryRight_apply, curry_uncurryRight, uncurry_curryRight
currySum 📖	CompOp	8 math math: currySum_add, currySumEquiv_apply, currySum_apply', uncurrySum_currySum, coe_currySumEquiv, currySum_smul, currySum_uncurrySum, currySum_apply
currySumEquiv 📖	CompOp	4 math math: currySumEquiv_apply, coe_currySumEquiv_symm, coe_currySumEquiv, currySumEquiv_symm_apply
uncurryRight 📖	CompOp	3 math math: curry_uncurryRight, uncurryRight_apply, uncurry_curryRight
uncurrySum 📖	CompOp	7 math math: coe_currySumEquiv_symm, uncurrySum_currySum, uncurrySum_add, uncurrySum_apply, currySum_uncurrySum, uncurrySum_smul, currySumEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_currySumEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike currySumEquiv currySum	—	smulCommClass_self RingHomInvPair.ids
coe_currySumEquiv_symm 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm currySumEquiv uncurrySum	—	smulCommClass_self RingHomInvPair.ids
curryFinFinset_apply 📖	mathematical	Finset.card Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike curryFinFinset Equiv Equiv.instEquivLike Equiv.symm finSumEquivOfFinset Fin.instLinearOrder	—	smulCommClass_self RingHomInvPair.ids
curryFinFinset_apply_const 📖	mathematical	Finset.card Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike curryFinFinset Finset.piecewise Finset.decidableMem	—	smulCommClass_self RingHomInvPair.ids curryFinFinset_symm_apply_piecewise_const LinearEquiv.symm_apply_apply
curryFinFinset_symm_apply 📖	mathematical	Finset.card Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm curryFinFinset Equiv Equiv.instEquivLike finSumEquivOfFinset Fin.instLinearOrder	—	smulCommClass_self RingHomInvPair.ids
curryFinFinset_symm_apply_const 📖	mathematical	Finset.card Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm curryFinFinset	—	smulCommClass_self RingHomInvPair.ids
curryFinFinset_symm_apply_piecewise_const 📖	mathematical	Finset.card Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Fin.fintype	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm curryFinFinset Finset.piecewise Finset.decidableMem	—	smulCommClass_self RingHomInvPair.ids curryFinFinset_symm_apply finSumEquivOfFinset_inl Finset.piecewise_eq_of_mem Finset.orderEmbOfFin_mem finSumEquivOfFinset_inr Finset.piecewise_eq_of_notMem Finset.mem_compl
curryLeft_apply 📖	mathematical	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike curryLeft Fin.cons	—	smulCommClass_self
curryMidLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap LinearMap Fin.succAbove addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid LinearMap.module instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike curryMidLinearEquiv curryMid	—	smulCommClass_self RingHomInvPair.ids
curryMidLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap MultilinearMap Fin.succAbove addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid LinearMap.module instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm curryMidLinearEquiv LinearMap.uncurryMid	—	smulCommClass_self RingHomInvPair.ids
curryMid_apply_apply 📖	mathematical	—	DFunLike.coe MultilinearMap Fin.succAbove CommSemiring.toSemiring instFunLikeForall LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike curryMid Fin.insertNth	—	smulCommClass_self
curryRight_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike MultilinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLikeForall curryRight Fin.snoc	—	smulCommClass_self
currySumEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike currySumEquiv currySum	—	smulCommClass_self RingHomInvPair.ids
currySumEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm currySumEquiv uncurrySum	—	smulCommClass_self RingHomInvPair.ids
currySum_add 📖	mathematical	—	currySum MultilinearMap CommSemiring.toSemiring instAdd addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
currySum_apply 📖	mathematical	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction currySum	—	smulCommClass_self
currySum_apply' 📖	mathematical	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction currySum	—	smulCommClass_self
currySum_smul 📖	mathematical	—	currySum MultilinearMap CommSemiring.toSemiring instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid addCommMonoid instModule instDistribMulActionOfSMulCommClass	—	smulCommClass_self
currySum_uncurrySum 📖	mathematical	—	currySum uncurrySum	—	smulCommClass_self
curry_uncurryRight 📖	mathematical	—	curryRight uncurryRight	—	smulCommClass_self ext LinearMap.ext Fin.snoc_last Fin.init_snoc
uncurryMid_curryMid 📖	mathematical	—	LinearMap.uncurryMid curryMid	—	ext Fin.insertNth_removeNth Function.update_eq_self
uncurryRight_apply 📖	mathematical	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall uncurryRight LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Fin.init	—	smulCommClass_self
uncurrySum_add 📖	mathematical	—	uncurrySum MultilinearMap CommSemiring.toSemiring addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instAdd	—	smulCommClass_self
uncurrySum_apply 📖	mathematical	—	DFunLike.coe MultilinearMap CommSemiring.toSemiring instFunLikeForall uncurrySum addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
uncurrySum_currySum 📖	mathematical	—	uncurrySum currySum	—	ext
uncurrySum_smul 📖	mathematical	—	uncurrySum MultilinearMap CommSemiring.toSemiring addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instDistribMulActionOfSMulCommClass	—	smulCommClass_self
uncurry_curryLeft 📖	mathematical	—	LinearMap.uncurryLeft curryLeft	—	ext Fin.cons_self_tail
uncurry_curryRight 📖	mathematical	—	uncurryRight curryRight	—	ext Fin.snoc_init_self

(root)

Definitions

Name	Category	Theorems
multilinearCurryLeftEquiv 📖	CompOp	2 math math: multilinearCurryLeftEquiv_apply, multilinearCurryLeftEquiv_symm_apply
multilinearCurryRightEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multilinearCurryLeftEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap LinearMap MultilinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid LinearMap.module MultilinearMap.instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike multilinearCurryLeftEquiv MultilinearMap.curryLeft	—	smulCommClass_self RingHomInvPair.ids
multilinearCurryLeftEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap MultilinearMap MultilinearMap.addCommMonoid MultilinearMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid LinearMap.module MultilinearMap.instDistribMulActionOfSMulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm multilinearCurryLeftEquiv LinearMap.uncurryLeft	—	smulCommClass_self RingHomInvPair.ids

---

← Back to Index