Documentation Verification Report

TensorProduct

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

Statistics

Metric	Count
Definitions `domCoprod`, `domCoprod'`, `domCoprodDep`, `domCoprodDep'`	4
Theorems `domCoprod'_apply`, `domCoprodDep'_apply`, `domCoprodDep_apply`, `domCoprod_apply`, `domCoprod_domDomCongr_sumCongr`	5
Total	9

MultilinearMap

Definitions

Name	Category	Theorems
`domCoprod` 📖	CompOp	7 math math: `AlternatingMap.domCoprod.summand_mk''`, `domCoprod_alternization_coe`, `domCoprod_domDomCongr_sumCongr`, `domCoprod_alternization_eq`, `domCoprod'_apply`, `domCoprod_apply`, `domCoprod_alternization`
`domCoprod'` 📖	CompOp	1 math math: `domCoprod'_apply`
`domCoprodDep` 📖	CompOp	2 math math: `domCoprodDep_apply`, `domCoprodDep'_apply`
`domCoprodDep'` 📖	CompOp	1 math math: `domCoprodDep'_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`domCoprod'_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `MultilinearMap` `addCommMonoid` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.instFunLike` `domCoprod'` `TensorProduct.tmul` `domCoprod`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left`
`domCoprodDep'_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `MultilinearMap` `addCommMonoid` `instModule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `LinearMap.instFunLike` `domCoprodDep'` `TensorProduct.tmul` `domCoprodDep`	—	`smulCommClass_self` `TensorProduct.smulCommClass_left`
`domCoprodDep_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLikeForall` `domCoprodDep` `TensorProduct.tmul`	—	—
`domCoprod_apply` 📖	mathematical	—	`DFunLike.coe` `MultilinearMap` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `instFunLikeForall` `domCoprod` `TensorProduct.tmul`	—	—
`domCoprod_domDomCongr_sumCongr` 📖	mathematical	—	`domDomCongr` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `Equiv.sumCongr` `domCoprod`	—	—

---

← Back to Index