Tower
📁 Source: FLT/Mathlib/Algebra/Algebra/Tower.lean
Statistics
| Metric | Count |
|---|---|
| 3 | |
| 3 | |
| Total | 6 |
AlgEquiv
Definitions
| Name | Category | Theorems |
|---|---|---|
changeScalars 📖 | CompOp | — |
extendScalars 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
extendScalars_apply 📖 | mathematical | — | extendScalars | — | — |
extendScalars_symm_apply 📖 | mathematical | — | extendScalars | — | — |
AlgHom
Definitions
| Name | Category | Theorems |
|---|---|---|
changeScalars 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
changeScalars_apply 📖 | mathematical | — | changeScalars | — | — |
---