Prod
📁 Source: Mathlib/RingTheory/Finiteness/Prod.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 2 | |
| Total | 2 |
Module.Finite
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
prod 📖 | mathematical | — | Module.FiniteProd.instAddCommMonoidProd.instModule | — | Submodule.prod_topSubmodule.FG.prodfg_top |
Submodule.FG
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
prod 📖 | mathematical | Submodule.FG | Prod.instAddCommMonoidProd.instModuleSubmodule.prod | — | Submodule.fg_defSet.Finite.unionSet.Finite.imageLinearMap.span_inl_union_inr |
---