Documentation Verification Report

TensorProduct

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

Statistics

Metric	Count
Definitions	0
Theorems `left_of_tensor`, `left_of_tensor_of_field`, `right_of_tensor`, `right_of_tensor_of_field`, `includeLeft_map_center_le`, `includeRight_map_center_le`	6
Total	6

Algebra.IsCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_of_tensor` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`Algebra.IsCentral`	—	`LE.le.trans` `Subalgebra.map_le` `Algebra.TensorProduct.includeLeft_map_center_le` `out` `Algebra.TensorProduct.includeLeft_injective` `smulCommClass_self`
`left_of_tensor_of_field` 📖	mathematical	—	`Algebra.IsCentral` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring`	—	`left_of_tensor` `FaithfulSMul.algebraMap_injective` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `Module.Flat.of_free`
`right_of_tensor` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`Algebra.IsCentral`	—	`of_algEquiv` `left_of_tensor`
`right_of_tensor_of_field` 📖	mathematical	—	`Algebra.IsCentral` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring`	—	`right_of_tensor` `FaithfulSMul.algebraMap_injective` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `Module.Flat.of_free`

Algebra.TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`includeLeft_map_center_le` 📖	mathematical	—	`Subalgebra` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instSemiring` `leftAlgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Subalgebra.map` `includeLeft` `Subalgebra.center` `instAlgebra`	—	`TensorProduct.induction_on` `Algebra.to_smulCommClass` `IsScalarTower.right` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `mul_one` `one_mul` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass`
`includeRight_map_center_le` 📖	mathematical	—	`Subalgebra` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instSemiring` `instAlgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `Subalgebra.map` `includeRight` `Subalgebra.center`	—	`TensorProduct.induction_on` `Algebra.to_smulCommClass` `IsScalarTower.right` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `mul_one` `one_mul` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass`

---

← Back to Index