Documentation Verification Report

Pi

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

Statistics

Metric	Count
Definitions `piRight`, `piRightHom`, `piScalarRight`, `prodRight`	4
Theorems `piRightHom_mul`, `piRightHom_one`, `piRight_tmul`, `piScalarRight_tmul`, `piScalarRight_tmul_apply`, `prodRight_symm_tmul`, `prodRight_tmul`, `prodRight_tmul_fst`, `prodRight_tmul_snd`, `piScalarRight_symm_algebraMap`	10
Total	14

Algebra.TensorProduct

Definitions

Name	Category	Theorems
`piRight` 📖	CompOp	1 math math: `piRight_tmul`
`piRightHom` 📖	CompOp	—
`piScalarRight` 📖	CompOp	2 math math: `piScalarRight_tmul`, `piScalarRight_tmul_apply`
`prodRight` 📖	CompOp	4 math math: `prodRight_tmul_fst`, `prodRight_symm_tmul`, `prodRight_tmul`, `prodRight_tmul_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piRightHom_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.addCommMonoid` `Algebra.toModule` `Pi.module` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `LinearMap.instFunLike` `TensorProduct.piRightHom` `instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `Pi.nonUnitalNonAssocSemiring` `Pi.semiring` `Pi.algebra` `Pi.instMul`	—	`TensorProduct.induction_on` `IsScalarTower.to_smulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `MulZeroClass.zero_mul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `MulZeroClass.mul_zero` `mul_add` `Distrib.leftDistribClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_mul` `Distrib.rightDistribClass`
`piRightHom_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.addCommMonoid` `Algebra.toModule` `Pi.module` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `LinearMap.instFunLike` `TensorProduct.piRightHom` `instOneTensorProduct` `NonAssocSemiring.toAddCommMonoidWithOne` `Pi.nonAssocSemiring` `Pi.instOne`	—	`IsScalarTower.to_smulCommClass`
`piRight_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Algebra.toModule` `Pi.module` `CommSemiring.toSemiring` `instSemiring` `Pi.semiring` `Pi.algebra` `leftAlgebra` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `piRight` `TensorProduct.tmul`	—	`IsScalarTower.to_smulCommClass`
`piScalarRight_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Pi.Function.module` `Semiring.toModule` `instSemiring` `Pi.semiring` `Function.algebra` `Algebra.id` `leftAlgebra` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `piScalarRight` `TensorProduct.tmul` `Algebra.toSMul`	—	`IsScalarTower.to_smulCommClass`
`piScalarRight_tmul_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Pi.Function.module` `Semiring.toModule` `instSemiring` `Pi.semiring` `Function.algebra` `Algebra.id` `leftAlgebra` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `piScalarRight` `TensorProduct.tmul` `Algebra.toSMul`	—	`IsScalarTower.to_smulCommClass`
`prodRight_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `Prod.instSemiring` `instSemiring` `Prod.algebra` `leftAlgebra` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `AlgEquiv.symm` `prodRight` `TensorProduct.tmul`	—	`AlgEquiv.injective` `IsScalarTower.to_smulCommClass` `AlgEquiv.apply_symm_apply`
`prodRight_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Algebra.toModule` `Prod.instModule` `CommSemiring.toSemiring` `instSemiring` `Prod.instSemiring` `Prod.algebra` `leftAlgebra` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `prodRight` `TensorProduct.tmul`	—	`IsScalarTower.to_smulCommClass`
`prodRight_tmul_fst` 📖	mathematical	—	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `DFunLike.coe` `AlgEquiv` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `instSemiring` `Prod.instSemiring` `Prod.algebra` `leftAlgebra` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `prodRight` `TensorProduct.tmul`	—	`IsScalarTower.to_smulCommClass`
`prodRight_tmul_snd` 📖	mathematical	—	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `DFunLike.coe` `AlgEquiv` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `instSemiring` `Prod.instSemiring` `Prod.algebra` `leftAlgebra` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `prodRight` `TensorProduct.tmul`	—	`IsScalarTower.to_smulCommClass`

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piScalarRight_symm_algebraMap` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.addCommMonoid` `Algebra.toModule` `Pi.Function.module` `Semiring.toModule` `addCommMonoid` `leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `piScalarRight` `RingHom` `Pi.commSemiring` `Pi.semiring` `RingHom.instFunLike` `algebraMap` `Pi.instAlgebraForall` `tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `Algebra.algebraMap_eq_smul_one` `piScalarRight_apply` `piScalarRightHom_tmul`

---

← Back to Index