TensorPi
📁 Source: FLT/DedekindDomain/FiniteAdeleRing/TensorPi.lean
Statistics
| Metric | Count |
|---|---|
| 6 | |
| 3 | |
| Total | 9 |
Module.FinitePresentation
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
exists_fin_exact 📖 | — | — | — | — | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
directSumPi_equiv_piSum 📖 | CompOp | — |
finsuppLeft_TensorPi_equiv_piTensor 📖 | CompOp | — |
freeModule_tensorPiEquiv 📖 | CompOp | — |
tensorPiEquiv_finitefreeModule 📖 | CompOp | — |
tensorPi_equiv_piTensor 📖 | CompOp | |
tensorPi_equiv_piTensor' 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
tensorPi_equiv_piTensor'_apply 📖 | mathematical | — | tensorPi_equiv_piTensor' | — | — |
tensorPi_equiv_piTensor_apply 📖 | mathematical | — | tensorPi_equiv_piTensor | — | directSumPi_equiv_piSum.eq_1 |
---