TensorProduct

📁 Source: Mathlib/Algebra/Star/TensorProduct.lean

Statistics

Metric	Count
Definitions instInvolutiveStar, instStar, instStarAddMonoid	3
Theorems instStarModule, star_tmul, starLinearEquiv_tensor	3
Total	6

TensorProduct

Definitions

Name	Category	Theorems
instInvolutiveStar 📖	CompOp	—
instStar 📖	CompOp	10 math math: Matrix.kroneckerTMulStarAlgEquiv_symm_apply, star_tmul, Matrix.toAlgEquiv_kroneckerStarAlgEquiv, Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv, instStarModule, Matrix.conjTranspose_kroneckerTMul, Matrix.kroneckerTMulStarAlgEquiv_apply, star_map_apply_eq_map_intrinsicStar, Matrix.kroneckerStarAlgEquiv_apply, Matrix.kroneckerStarAlgEquiv_symm_apply
instStarAddMonoid 📖	CompOp	6 math math: Pi.intrinsicStar_comul_commSemiring, LinearMap.intrinsicStar_mul', LinearMap.intrinsicStar_rTensor, intrinsicStar_map, starLinearEquiv_tensor, LinearMap.intrinsicStar_lTensor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarModule 📖	mathematical	—	StarModule TensorProduct InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid instStar instSMul	—	MulActionSemiHomClass.map_smulₛₗ RingHomInvPair.instStarRingEnd SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
star_tmul 📖	mathematical	—	Star.star TensorProduct instStar tmul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
starLinearEquiv_tensor 📖	mathematical	—	starLinearEquiv TensorProduct TensorProduct.addCommMonoid TensorProduct.instStarAddMonoid TensorProduct.instModule TensorProduct.instStarModule TensorProduct.congr starRingEnd RingHomInvPair.instStarRingEnd	—	RingHomInvPair.instStarRingEnd TensorProduct.instStarModule

---

← Back to Index