Pi

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

Statistics

Metric	Count
Definitions piLeft, piRight, piRightHom, piScalarRight, piScalarRightHom	5
Theorems piRightHom_tmul, piRight_apply, piRight_symm_apply, piRight_symm_single, piScalarRightHom_tmul, piScalarRight_apply, piScalarRight_symm_single	7
Total	12

TensorProduct

Definitions

Name	Category	Theorems
piLeft 📖	CompOp	1 math math: Ideal.pi_mkQ_rTensor
piRight 📖	CompOp	3 math math: piRight_symm_apply, piRight_symm_single, piRight_apply
piRightHom 📖	CompOp	4 math math: Algebra.TensorProduct.piRightHom_mul, piRightHom_tmul, Algebra.TensorProduct.piRightHom_one, piRight_apply
piScalarRight 📖	CompOp	4 math math: piScalarRight_symm_algebraMap, piScalarRight_symm_single, Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply, piScalarRight_apply
piScalarRightHom 📖	CompOp	3 math math: piScalarRight_apply, piScalarRightHom_tmul, Algebra.TensorProduct.equivPiOfFiniteBasis_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piRightHom_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Pi.addCommMonoid Pi.module addCommMonoid leftModule IsScalarTower.to_smulCommClass LinearMap.instFunLike piRightHom tmul	—	IsScalarTower.to_smulCommClass
piRight_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Pi.addCommMonoid Pi.module addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike piRight LinearMap LinearMap.instFunLike piRightHom	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
piRight_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Pi.addCommMonoid Pi.module addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm piRight tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
piRight_symm_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Pi.addCommMonoid Pi.module addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm piRight Pi.single zero tmul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
piScalarRightHom_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid leftModule IsScalarTower.to_smulCommClass LinearMap.instFunLike piScalarRightHom tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsScalarTower.to_smulCommClass
piScalarRight_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike piScalarRight LinearMap LinearMap.instFunLike piScalarRightHom	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
piScalarRight_symm_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm piScalarRight Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid tmul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass

---

← Back to Index