Documentation Verification Report

TensorProduct

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

Statistics

Metric	Count
Definitions `directSum`, `directSumLeft`, `directSumRight`, `directSumRight'`	4
Theorems `coe_directSumRight`, `coe_directSumRight'`, `directSumLeft_symm_lof_tmul`, `directSumLeft_tmul`, `directSumLeft_tmul_lof`, `directSumRight'_restrict`, `directSumRight_comp_rTensor`, `directSumRight_symm_lof_tmul`, `directSumRight_tmul`, `directSumRight_tmul_lof`, `directSum_lof_tmul_lof`, `directSum_symm_lof_tmul`, `restrictScalar_directSumRight`	13
Total	17

TensorProduct

Definitions

Name	Category	Theorems
`directSum` 📖	CompOp	2 math math: `directSum_lof_tmul_lof`, `directSum_symm_lof_tmul`
`directSumLeft` 📖	CompOp	3 math math: `directSumLeft_tmul_lof`, `directSumLeft_symm_lof_tmul`, `directSumLeft_tmul`
`directSumRight` 📖	CompOp	8 math math: `coe_directSumRight'`, `directSumRight_comp_rTensor`, `directSumRight_tmul_lof`, `directSumRight_tmul`, `directSumRight'_restrict`, `coe_directSumRight`, `directSumRight_symm_lof_tmul`, `restrictScalar_directSumRight`
`directSumRight'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_directSumRight` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directSumRight` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `LinearMap.IsScalarTower.compatibleSMul` `isScalarTower_left` `DirectSum.instIsScalarTower` `restrictScalar_directSumRight`
`coe_directSumRight'` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directSumRight` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`coe_directSumRight`
`directSumLeft_symm_lof_tmul` 📖	mathematical	`IsScalarTower` `Algebra.toSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `CommSemiring.toSemiring`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectSum` `TensorProduct` `addCommMonoid` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `leftModule` `IsScalarTower.to_smulCommClass` `DirectSum.instSMulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `directSumLeft` `LinearMap` `LinearMap.instFunLike` `DirectSum.lof` `tmul`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `DirectSum.instSMulCommClass` `LinearEquiv.symm_apply_eq` `directSumLeft_tmul_lof`
`directSumLeft_tmul` 📖	mathematical	`IsScalarTower` `Algebra.toSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `CommSemiring.toSemiring`	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct` `DFinsupp.instDFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `DirectSum.instSMulCommClass` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directSumLeft` `tmul`	—	`IsScalarTower.to_smulCommClass` `RingHomCompTriple.ids` `DirectSum.instSMulCommClass` `RingHomInvPair.ids` `SMulCommClass.symm` `smulCommClass_left` `DirectSum.linearMap_ext` `LinearMap.ext` `directSumLeft_tmul_lof` `DirectSum.component.lof_self` `DirectSum.component.of` `tmul_add` `zero_tmul` `LinearMap.congr_fun`
`directSumLeft_tmul_lof` 📖	mathematical	`IsScalarTower` `Algebra.toSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `CommSemiring.toSemiring`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `DirectSum.instSMulCommClass` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directSumLeft` `tmul` `LinearMap` `LinearMap.instFunLike` `DirectSum.lof`	—	`RingHomInvPair.ids` `DirectSum.instSMulCommClass` `IsScalarTower.to_smulCommClass` `Unique.instSubsingleton` `DirectSum.lid_symm_apply` `directSum_lof_tmul_lof` `DirectSum.lequivCongrLeft_lof`
`directSumRight'_restrict` 📖	mathematical	—	`LinearEquiv.restrictScalars` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `IsScalarTower.to_smulCommClass` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `isScalarTower_left` `DirectSum.instIsScalarTower` `directSumRight`	—	`restrictScalar_directSumRight`
`directSumRight_comp_rTensor` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `leftModule` `IsScalarTower.to_smulCommClass` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `directSumRight` `LinearMap.rTensor` `DirectSum.lmap`	—	`AlgebraTensorModule.curry_injective` `IsScalarTower.left` `IsScalarTower.to_smulCommClass` `DirectSum.instIsScalarTower` `isScalarTower` `smulCommClass_self` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext` `DirectSum.linearMap_ext` `DirectSum.ext` `directSumRight_tmul_lof` `DirectSum.lmap_lof`
`directSumRight_symm_lof_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectSum` `TensorProduct` `addCommMonoid` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `directSumRight` `LinearMap` `LinearMap.instFunLike` `DirectSum.lof` `tmul`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `LinearEquiv.symm_apply_eq` `directSumRight_tmul_lof`
`directSumRight_tmul` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct` `DFinsupp.instDFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directSumRight` `tmul`	—	`RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass` `LinearMap.IsScalarTower.compatibleSMul` `DirectSum.instIsScalarTower` `isScalarTower_left` `smulCommClass_self` `RingHomInvPair.ids` `smulCommClass_left` `DirectSum.linearMap_ext` `LinearMap.ext` `directSumRight_tmul_lof` `DirectSum.component.lof_self` `DirectSum.component.of` `tmul_zero` `LinearMap.congr_fun`
`directSumRight_tmul_lof` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directSumRight` `tmul` `LinearMap` `LinearMap.instFunLike` `DirectSum.lof`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `Unique.instSubsingleton` `DirectSum.lid_symm_apply` `directSum_lof_tmul_lof` `DirectSum.lequivCongrLeft_lof`
`directSum_lof_tmul_lof` 📖	mathematical	`IsScalarTower` `Algebra.toSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `CommSemiring.toSemiring`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `DirectSum.instSMulCommClass` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `directSum` `tmul` `LinearMap` `LinearMap.instFunLike` `DirectSum.lof`	—	`RingHomInvPair.ids` `DirectSum.instSMulCommClass` `IsScalarTower.to_smulCommClass` `smulCommClass_self` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.instIsScalarTower` `DirectSum.toModule_lof`
`directSum_symm_lof_tmul` 📖	mathematical	`IsScalarTower` `Algebra.toSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `CommSemiring.toSemiring`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DirectSum` `TensorProduct` `addCommMonoid` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `leftModule` `IsScalarTower.to_smulCommClass` `DirectSum.instSMulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `directSum` `LinearMap` `LinearMap.instFunLike` `DirectSum.lof` `tmul`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `DirectSum.instSMulCommClass` `LinearEquiv.symm_apply_eq` `directSum_lof_tmul_lof`
`restrictScalar_directSumRight` 📖	mathematical	—	`LinearEquiv.restrictScalars` `TensorProduct` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `addCommMonoid` `leftModule` `IsScalarTower.to_smulCommClass` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `isScalarTower_left` `DirectSum.instIsScalarTower` `directSumRight`	—	`LinearEquiv.restrictScalars_injective` `IsScalarTower.to_smulCommClass` `LinearMap.IsScalarTower.compatibleSMul` `isScalarTower_left` `DirectSum.instIsScalarTower` `smulCommClass_self` `LinearEquiv.toLinearMap_injective` `RingHomInvPair.ids` `AlgebraTensorModule.curry_injective` `IsScalarTower.left` `isScalarTower` `LinearMap.ext` `DirectSum.linearMap_ext` `RingHomCompTriple.ids` `DirectSum.ext` `directSumRight_tmul`

---

← Back to Index