Basic
📁 Source: FLT/Mathlib/Algebra/FixedPoints/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsFixedPoints, instCoeHead, FixedPoints, addCommGroup, addCommMonoid, addGroup, addMonoid, addZeroClass, instCoeHead, module | 10 |
| 7 | |
| Total | 17 |
AddAction
Definitions
| Name | Category | Theorems |
|---|---|---|
FixedPoints 📖 | CompOp | — |
AddAction.FixedPoints
Definitions
| Name | Category | Theorems |
|---|---|---|
instCoeHead 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
ext 📖 | — | — | — | — | — |
ext_iff 📖 | — | — | — | — | ext |
MulAction
Definitions
| Name | Category | Theorems |
|---|---|---|
FixedPoints 📖 | CompOp |
MulAction.FixedPoints
Definitions
| Name | Category | Theorems |
|---|---|---|
addCommGroup 📖 | CompOp | — |
addCommMonoid 📖 | CompOp | — |
addGroup 📖 | CompOp | — |
addMonoid 📖 | CompOp | — |
addZeroClass 📖 | CompOp | |
instCoeHead 📖 | CompOp | — |
module 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
coe_add 📖 | mathematical | — | MulAction.FixedPointsaddZeroClass | — | — |
ext 📖 | — | — | — | — | — |
ext_iff 📖 | — | — | — | — | ext |
smul_neg 📖 | — | — | — | — | — |
zero_def 📖 | mathematical | — | MulAction.FixedPointsaddZeroClass | — | — |
---