Prod

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Prod.lean

Statistics

Metric	Count
Definitions prodLeft, prodRight	2
Theorems prodLeft_symm_tmul, prodLeft_tmul, prodRight_symm_tmul, prodRight_tmul	4
Total	6

TensorProduct

Definitions

Name	Category	Theorems
prodLeft 📖	CompOp	2 math math: prodLeft_tmul, prodLeft_symm_tmul
prodRight 📖	CompOp	2 math math: prodRight_symm_tmul, prodRight_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodLeft_symm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Prod.instAddCommMonoid Prod.instModule CommSemiring.toSemiring addCommMonoid leftModule IsScalarTower.to_smulCommClass Prod.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm prodLeft tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass Prod.smulCommClass LinearEquiv.symm_apply_eq
prodLeft_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Prod.instAddCommMonoid Prod.instModule CommSemiring.toSemiring addCommMonoid leftModule Prod.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike prodLeft tmul	—	RingHomInvPair.ids Prod.smulCommClass IsScalarTower.to_smulCommClass
prodRight_symm_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Prod.instAddCommMonoid Prod.instModule CommSemiring.toSemiring addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm prodRight tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass LinearEquiv.symm_apply_eq
prodRight_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Prod.instAddCommMonoid Prod.instModule CommSemiring.toSemiring addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike prodRight tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass

---

← Back to Index