Revision #1133 → #2282 · back to history
addedConnected covering is surjective with constant fiber cardinalityfa5805191d98
modifiedFactorisation of coverings (first)85b18570aaa1
| Field | From #1133 | To #2282 |
|---|
| note | No composition lemma for `IsCoveringMap` exists; grep for `IsCoveringMap.comp` returns nothing. | No composition lemma for `IsCoveringMap` exists; `IsCoveringMap.comp` is absent. |
modifiedBranched covering of degree naad1f1a52dc8
| Field | From #1133 | To #2282 |
|---|
| note | Not formalized as branched covering, though `isCoveringMapOn_npow` covers the unramified locus. | Not formalized as branched covering, though `isCoveringMap_npow` covers the unramified locus. |
addedUniversal cover unique up to equivalencecc8798d7c7de
addedSO(3) is RP³ with Spin(3) = S³ as universal covera024ebef25c2