| changeset 72632 | 773ad766f1b8 |
| parent 70097 | 4005298550a6 |
| child 73932 | fd21b4a93043 |
| 72631:bafc0ec0e018 | 72632:773ad766f1b8 |
|---|---|
1 section\<open>Homology, III: Brouwer Degree\<close> |
1 section\<open>Homology, III: Brouwer Degree\<close> |
2 |
2 |
3 theory Brouwer_Degree |
3 theory Brouwer_Degree |
4 imports Homology_Groups |
4 imports Homology_Groups "HOL-Algebra.Multiplicative_Group" |
5 |
5 |
6 begin |
6 begin |
7 |
7 |
8 subsection\<open>Reduced Homology\<close> |
8 subsection\<open>Reduced Homology\<close> |
9 |
9 |