Curry

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

Statistics

Metric	Count
Definitions curryLeft, curryLeftLinearMap	2
Theorems curryLeftLinearMap_apply, curryLeft_add, curryLeft_apply_apply, curryLeft_apply_toMultilinearMap, curryLeft_compAlternatingMap, curryLeft_compLinearMap, curryLeft_same, curryLeft_smul, curryLeft_zero	9
Total	11

AlternatingMap

Definitions

Name	Category	Theorems
curryLeft 📖	CompOp	14 math math: uncurryFin_curryLeft, ExteriorAlgebra.liftAlternating_ι_mul, ContinuousAlternatingMap.toAlternatingMap_curryLeft, curryLeft_apply_apply, curryLeft_apply_toMultilinearMap, alternatizeUncurryFin_curryLeft, curryLeft_zero, curryLeftLinearMap_apply, curryLeft_smul, curryLeft_compAlternatingMap, curryLeft_compLinearMap, ExteriorAlgebra.ιMulti_succ_curryLeft, curryLeft_add, curryLeft_same
curryLeftLinearMap 📖	CompOp	1 math math: curryLeftLinearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curryLeftLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid LinearMap.module instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike curryLeftLinearMap curryLeft	—	smulCommClass_self instSMulCommClass
curryLeft_add 📖	mathematical	—	curryLeft AlternatingMap CommSemiring.toSemiring instAdd LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instAdd	—	smulCommClass_self
curryLeft_apply_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring instFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike curryLeft Matrix.vecCons	—	smulCommClass_self
curryLeft_apply_toMultilinearMap 📖	mathematical	—	toMultilinearMap CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AlternatingMap instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike curryLeft MultilinearMap MultilinearMap.addCommMonoid MultilinearMap.instModule MultilinearMap.curryLeft	—	smulCommClass_self
curryLeft_compAlternatingMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike curryLeft LinearMap.compAlternatingMap	—	smulCommClass_self
curryLeft_compLinearMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike curryLeft compLinearMap	—	ext smulCommClass_self Fin.cons_zero Fin.cons_succ
curryLeft_same 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike curryLeft instZero	—	ext smulCommClass_self map_eq_zero_of_eq Fin.cons_zero Fin.cons_one
curryLeft_smul 📖	mathematical	—	curryLeft AlternatingMap CommSemiring.toSemiring instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule LinearMap.instSMul DistribMulAction.toDistribSMul instDistribMulAction instSMulCommClass	—	smulCommClass_self
curryLeft_zero 📖	mathematical	—	curryLeft AlternatingMap CommSemiring.toSemiring instZero LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instZero	—	smulCommClass_self

---

← Back to Index