TensorProduct
📁 Source: FLT/Mathlib/RingTheory/SimpleRing/TensorProduct.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 8 | |
| Total | 8 |
Submodule
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
mem_span_range_iff_exists 📖 | — | — | — | — | — |
TensorProduct
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
map_comap_eq 📖 | — | — | — | — | TwoSidedIdeal.map.eq_1TwoSidedIdeal.eq_bot_of_map_comap_eq_botTwoSidedIdeal.map_bot |
simple 📖 | — | — | — | — | map_comap_eqTwoSidedIdeal.map.eq_1TwoSidedIdeal.span_eq_bot |
TwoSidedIdeal
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
eq_bot_of_map_comap_eq_bot 📖 | — | — | — | — | mem_map_of_memSubmodule.mem_span_range_iff_exists |
map_bot 📖 | — | — | — | — | span_singleton_eq_bot |
mem_map_of_mem 📖 | — | — | — | — | — |
span_eq_bot 📖 | — | — | — | — | — |
span_singleton_eq_bot 📖 | — | — | — | — | — |
---