Documentation Verification Report

PiTensorProduct

📁 Source: PhysLean/Mathematics/PiTensorProduct.lean

Statistics

Metric	Count
Definitions `domCoprod`, `elimPureTensor`, `elimPureTensorMulLin`, `instAddCommMonoidElim_physLean`, `instModuleElim_physLean`, `pureInl`, `pureInr`, `tmul`, `tmulEquiv`, `tmulSymm`	10
Theorems `elimPureTensor_update_left`, `elimPureTensor_update_right`, `induction_assoc`, `induction_assoc'`, `induction_mod_tmul`, `induction_tmul`, `induction_tmul_mod`, `pureInl_update_left`, `pureInl_update_right`, `pureInr_update_left`, `pureInr_update_right`, `tmulEquiv_tmul_tprod`	12
Total	22

PhysLean.PiTensorProduct

Definitions

Name	Category	Theorems
`domCoprod` 📖	CompOp	—
`elimPureTensor` 📖	CompOp	7 math math: `IndexNotation.OverColor.lift.μ_tmul_tprod`, `elimPureTensor_update_right`, `IndexNotation.OverColor.lift.μ_tmul_tprod_mk`, `elimPureTensor_update_left`, `tmulEquiv_tmul_tprod`, `IndexNotation.OverColor.lift.μModEquiv_tmul_tprod`, `IndexNotation.OverColor.lift.obj_μ_tprod_tmul`
`elimPureTensorMulLin` 📖	CompOp	—
`instAddCommMonoidElim_physLean` 📖	CompOp	5 math math: `IndexNotation.OverColor.lift.μ_tmul_tprod`, `IndexNotation.OverColor.lift.μ_tmul_tprod_mk`, `tmulEquiv_tmul_tprod`, `IndexNotation.OverColor.lift.μModEquiv_tmul_tprod`, `IndexNotation.OverColor.lift.obj_μ_tprod_tmul`
`instModuleElim_physLean` 📖	CompOp	5 math math: `IndexNotation.OverColor.lift.μ_tmul_tprod`, `IndexNotation.OverColor.lift.μ_tmul_tprod_mk`, `tmulEquiv_tmul_tprod`, `IndexNotation.OverColor.lift.μModEquiv_tmul_tprod`, `IndexNotation.OverColor.lift.obj_μ_tprod_tmul`
`pureInl` 📖	CompOp	2 math math: `pureInl_update_right`, `pureInl_update_left`
`pureInr` 📖	CompOp	2 math math: `pureInr_update_right`, `pureInr_update_left`
`tmul` 📖	CompOp	—
`tmulEquiv` 📖	CompOp	1 math math: `tmulEquiv_tmul_tprod`
`tmulSymm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elimPureTensor_update_left` 📖	mathematical	—	`elimPureTensor`	—	—
`elimPureTensor_update_right` 📖	mathematical	—	`elimPureTensor`	—	—
`induction_assoc` 📖	—	—	—	—	—
`induction_assoc'` 📖	—	—	—	—	—
`induction_mod_tmul` 📖	—	—	—	—	—
`induction_tmul` 📖	—	—	—	—	—
`induction_tmul_mod` 📖	—	—	—	—	—
`pureInl_update_left` 📖	mathematical	—	`pureInl`	—	—
`pureInl_update_right` 📖	mathematical	—	`pureInl`	—	—
`pureInr_update_left` 📖	mathematical	—	`pureInr`	—	—
`pureInr_update_right` 📖	mathematical	—	`pureInr`	—	—
`tmulEquiv_tmul_tprod` 📖	mathematical	—	`instAddCommMonoidElim_physLean` `instModuleElim_physLean` `tmulEquiv` `elimPureTensor`	—	—

---

← Back to Index