Quotient
📁 Source: FLT/Mathlib/Topology/Algebra/Group/Quotient.lean
Statistics
| Metric | Count |
|---|---|
| 2 | |
TheoremsisOpenQuotientMap_rightrel_mk | 1 |
| Total | 3 |
QuotientAddGroup
Definitions
| Name | Category | Theorems |
|---|---|---|
continuousAddEquiv 📖 | CompOp | — |
QuotientGroup
Definitions
| Name | Category | Theorems |
|---|---|---|
continuousMulEquiv 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
isOpenQuotientMap_rightrel_mk 📖 | — | — | — | — | — |
---