| changeset 72632 | 773ad766f1b8 |
| parent 70097 | 4005298550a6 |
| child 73932 | fd21b4a93043 |
--- a/src/HOL/Homology/Brouwer_Degree.thy Mon Nov 16 21:37:32 2020 +0000 +++ b/src/HOL/Homology/Brouwer_Degree.thy Tue Nov 17 09:57:25 2020 +0000 @@ -1,7 +1,7 @@ section\<open>Homology, III: Brouwer Degree\<close> theory Brouwer_Degree - imports Homology_Groups + imports Homology_Groups "HOL-Algebra.Multiplicative_Group" begin