Pairing

📁 Source: Mathlib/LinearAlgebra/TensorPower/Pairing.lean

Statistics

Metric	Count
Definitions Pairing, multilinearMapToDual, pairingDual	3
Theorems multilinearMapToDual_apply_tprod, pairingDual_tprod_tprod	2
Total	5

SSet.Subcomplex

Definitions

Name	Category	Theorems
Pairing 📖	CompData	—

TensorPower

Definitions

Name	Category	Theorems
multilinearMapToDual 📖	CompOp	1 math math: multilinearMapToDual_apply_tprod
pairingDual 📖	CompOp	1 math math: pairingDual_tprod_tprod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multilinearMapToDual_apply_tprod 📖	mathematical	—	DFunLike.coe Module.Dual TensorPower CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MultilinearMap LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id MultilinearMap.instFunLikeForall multilinearMapToDual PiTensorProduct PiTensorProduct.tprod Finset.prod CommSemiring.toCommMonoid Finset.univ Fin.fintype	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self PiTensorProduct.lift.tprod mul_one
pairingDual_tprod_tprod 📖	mathematical	—	DFunLike.coe Module.Dual TensorPower CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id pairingDual MultilinearMap PiTensorProduct MultilinearMap.instFunLikeForall PiTensorProduct.tprod Finset.prod CommSemiring.toCommMonoid Finset.univ Fin.fintype	—	Algebra.to_smulCommClass PiTensorProduct.lift.tprod multilinearMapToDual_apply_tprod

---

← Back to Index