Skip to content

Commit 9940158

Browse files
committed
Explicitly import Commutative
1 parent c4cea19 commit 9940158

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Algebra/NormalSubgroup.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open import Algebra.Bundles using (Group)
1010

1111
module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ) where
1212

13-
open import Algebra.Definitions
13+
open import Algebra.Definitions using (Commutative)
1414
open import Algebra.Construct.Sub.Group G using (Subgroup)
1515
open import Level using (suc; _⊔_)
1616

0 commit comments

Comments
 (0)