Coevaluation

📁 Source: Mathlib/LinearAlgebra/Coevaluation.lean

Statistics

Metric	Count
Definitions coevaluation	1
Theorems coevaluation_apply_one, contractLeft_assoc_coevaluation, contractLeft_assoc_coevaluation'	3
Total	4

(root)

Definitions

Name	Category	Theorems
coevaluation 📖	CompOp	3 math math: contractLeft_assoc_coevaluation, coevaluation_apply_one, contractLeft_assoc_coevaluation'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coevaluation_apply_one 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module CommSemiring.toSemiring Algebra.to_smulCommClass Algebra.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike coevaluation AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Algebra.to_smulCommClass RingHomInvPair.ids Finite.of_fintype Module.Basis.constr_apply_fintype Finset.sum_congr Module.Basis.singleton_repr Module.Basis.coe_ofVectorSpace one_smul Finset.sum_const Finset.card_singleton
contractLeft_assoc_coevaluation 📖	mathematical	—	LinearMap.comp TensorProduct Semifield.toCommSemiring Field.toSemifield Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain LinearMap.module CommSemiring.toSemiring Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule RingHomCompTriple.ids LinearMap.rTensor contractLeft LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm TensorProduct.assoc LinearMap.lTensor coevaluation TensorProduct.lid TensorProduct.rid	—	TensorProduct.ext Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids Module.Basis.ext smulCommClass_self Finite.of_fintype LinearMap.ext_ring LinearMap.compr₂ₛₗ_apply TensorProduct.smulCommClass_left TensorProduct.mk_apply TensorProduct.rid_tmul one_smul TensorProduct.lid_symm_apply coevaluation_apply_one TensorProduct.tmul_sum map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finset.sum_congr LinearMap.semilinearMapClass Module.Basis.coe_dualBasis Module.Basis.repr_self_apply TensorProduct.ite_tmul Finset.sum_ite_eq'
contractLeft_assoc_coevaluation' 📖	mathematical	—	LinearMap.comp TensorProduct Semifield.toCommSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid Semiring.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule RingHomCompTriple.ids LinearMap.lTensor contractLeft LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.assoc LinearMap.rTensor coevaluation LinearEquiv.symm TensorProduct.rid TensorProduct.lid	—	TensorProduct.ext Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext_ring smulCommClass_self Module.Basis.ext LinearMap.compr₂ₛₗ_apply TensorProduct.smulCommClass_left TensorProduct.mk_apply TensorProduct.lid_tmul one_smul TensorProduct.rid_symm_apply coevaluation_apply_one TensorProduct.sum_tmul map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finset.sum_congr LinearMap.semilinearMapClass Module.Basis.repr_self_apply TensorProduct.tmul_ite Finset.sum_ite_eq

---

← Back to Index