Ring
📁 Source: ClassFieldTheory/Mathlib/RingTheory/AdicCompletion/Ring.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsmkRing | 1 |
| 6 | |
| Total | 7 |
AdicCompletion
Definitions
| Name | Category | Theorems |
|---|---|---|
mkRing 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
mk_ofLinearEquiv_symm_mkRing 📖 | mathematical | — | mkRing | — | Ideal.quotEquivOfEq_transIdeal.quotEquivOfEq_rfl |
Ideal
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
quotEquivOfEq_rfl 📖 | — | — | — | — | — |
quotEquivOfEq_trans 📖 | — | — | — | — | — |
Ideal.Quotient
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
factorPow_comp_factorPow 📖 | — | — | — | — | — |
IsHausdorff
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
eq_iff_eq 📖 | — | — | — | — | — |
Submodule
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
factorPow_eq_factorPow 📖 | — | — | — | — | — |
---