Documentation Verification Report

TensorProduct

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

Statistics

Metric	Count
Definitions `includeRight`, `liftEquiv`, `baseChange`, `instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat`, `instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat_1`, `instCommRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat`, `instCommSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat`, `instRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat`, `instSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat`	9
Theorems `includeRight_apply`, `liftEquiv_symm_apply`, `liftEquiv_tmul`, `algebraMap_apply`, `coe_algebraMap_apply`	5
Total	14

GradedAlgHom

Definitions

Name	Category	Theorems
`includeRight` 📖	CompOp	1 math math: `includeRight_apply`
`liftEquiv` 📖	CompOp	2 math math: `liftEquiv_symm_apply`, `liftEquiv_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`includeRight_apply` 📖	mathematical	—	`DFunLike.coe` `GradedAlgHom` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Submodule.restrictScalars` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.toSMul` `TensorProduct.isScalarTower_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `Submodule.baseChange` `instGradedAlgebraRestrictScalars` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `GradedAlgebra.baseChange` `instFunLike` `includeRight` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Algebra.to_smulCommClass` `TensorProduct.isScalarTower_left` `IsScalarTower.right`
`liftEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `GradedAlgHom` `Submodule.restrictScalars` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.toSMul` `instGradedAlgebraRestrictScalars` `instFunLike` `Equiv` `TensorProduct` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `Submodule.baseChange` `GradedAlgebra.baseChange` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `liftEquiv` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Algebra.to_smulCommClass`
`liftEquiv_tmul` 📖	mathematical	—	`DFunLike.coe` `GradedAlgHom` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `Submodule.baseChange` `GradedAlgebra.baseChange` `instFunLike` `Equiv` `Submodule.restrictScalars` `Algebra.toSMul` `instGradedAlgebraRestrictScalars` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftEquiv` `TensorProduct.tmul`	—	`Algebra.to_smulCommClass`

GradedAlgebra

Definitions

Name	Category	Theorems
`baseChange` 📖	CompOp	3 math math: `GradedAlgHom.includeRight_apply`, `GradedAlgHom.liftEquiv_symm_apply`, `GradedAlgHom.liftEquiv_tmul`
`instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat` 📖	CompOp	1 math math: `coe_algebraMap_apply`
`instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat_1` 📖	CompOp	1 math math: `algebraMap_apply`
`instCommRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat` 📖	CompOp	—
`instCommSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat` 📖	CompOp	1 math math: `algebraMap_apply`
`instRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat` 📖	CompOp	—
`instSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat` 📖	CompOp	1 math math: `coe_algebraMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Submodule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `SetLike.instMembership` `Submodule.setLike` `Submodule.baseChange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instCommSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat` `Algebra.TensorProduct.instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat_1`	—	`Algebra.to_smulCommClass`
`coe_algebraMap_apply` 📖	mathematical	—	`TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Submodule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `SetLike.instMembership` `Submodule.setLike` `Submodule.baseChange` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `RingHom` `instSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat` `RingHom.instFunLike` `algebraMap` `instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Algebra.to_smulCommClass`

---

← Back to Index