TensorProduct

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

Statistics

Metric	Count
Definitions baseChange, tensorDistrib, tensorDistribEquiv, tmul, baseChange, tensorDistrib, tmul	7
Theorems baseChange, baseChange_tmul, tensorDistribEquiv_apply, tensorDistribEquiv_tmul, tensorDistribEquiv_toLinearMap, tensorDistrib_tmul, baseChange_isSymm, baseChange_tmul, tensorDistrib_tmul, tmul_isSymm, tmul	11
Total	18

LinearMap.BilinForm

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	4 math math: QuadraticForm.polarBilin_baseChange, IsSymm.baseChange, baseChange_tmul, QuadraticForm.associated_baseChange
tensorDistrib 📖	CompOp	3 math math: tensorDistribEquiv_toLinearMap, tensorDistrib_tmul, tensorDistribEquiv_apply
tensorDistribEquiv 📖	CompOp	3 math math: tensorDistribEquiv_toLinearMap, tensorDistribEquiv_apply, tensorDistribEquiv_tmul
tmul 📖	CompOp	3 math math: QuadraticForm.polarBilin_tmul, LinearMap.IsSymm.tmul, QuadraticForm.associated_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module baseChange TensorProduct.tmul Algebra.toSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Algebra.to_smulCommClass
tensorDistribEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap.BilinForm AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv tensorDistribEquiv Algebra.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right TensorProduct.leftModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing LinearMap.instFunLike tensorDistrib IsScalarTower.left	—	Algebra.to_smulCommClass LinearMap.instSMulCommClass DFunLike.congr_fun RingHomInvPair.ids IsScalarTower.left tensorDistribEquiv_toLinearMap
tensorDistribEquiv_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct AddCommGroup.toAddCommMonoid TensorProduct.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct.instModule Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module LinearEquiv RingHomInvPair.ids Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv tensorDistribEquiv TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids Algebra.to_smulCommClass LinearMap.instSMulCommClass
tensorDistribEquiv_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct LinearMap.BilinForm AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.addCommMonoid TensorProduct.instModule tensorDistribEquiv tensorDistrib IsScalarTower.left DistribMulAction.toMulAction	—	TensorProduct.AlgebraTensorModule.curry_injective Algebra.to_smulCommClass LinearMap.instSMulCommClass LinearMap.instIsScalarTower IsScalarTower.right RingHomInvPair.ids IsScalarTower.left LinearMap.ext IsScalarTower.to_smulCommClass mul_comm
tensorDistrib_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct TensorProduct.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct.leftModule Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module Algebra.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id tensorDistrib TensorProduct.tmul Algebra.toSMul	—	IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instSMulCommClass Algebra.to_smulCommClass

LinearMap.BilinForm.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	LinearMap.IsSymm RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.BilinForm.baseChange	—	LinearMap.IsSymm.tmul mul_comm

LinearMap.BilinMap

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	2 math math: baseChange_isSymm, baseChange_tmul
tensorDistrib 📖	CompOp	1 math math: tensorDistrib_tmul
tmul 📖	CompOp	2 math math: tmul_isSymm, QuadraticMap.associated_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_isSymm 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass baseChange	—	tmul_isSymm mul_comm
baseChange_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module baseChange TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Algebra.to_smulCommClass
tensorDistrib_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid TensorProduct.smulCommClass_left tensorDistrib TensorProduct.tmul	—	IsScalarTower.to_smulCommClass' LinearMap.instSMulCommClass smulCommClass_self TensorProduct.smulCommClass_left
tmul_isSymm 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.BilinMap LinearMap.addCommMonoid LinearMap.module	TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule tmul	—	isSymm_iff_eq_flip TensorProduct.AlgebraTensorModule.curry_injective TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' LinearMap.instIsScalarTower TensorProduct.isScalarTower_left LinearMap.ext IsScalarTower.to_smulCommClass

LinearMap.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tmul 📖	mathematical	LinearMap.IsSymm RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule LinearMap.BilinForm.tmul	—	LinearMap.isSymm_iff_eq_flip TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.to_smulCommClass' IsScalarTower.right LinearMap.instIsScalarTower LinearMap.ext IsScalarTower.to_smulCommClass Algebra.to_smulCommClass eq

---

← Back to Index