Skip to content

Commit c87e4bf

Browse files
committed
Add _/_ synomym for quotient group
1 parent 60616c1 commit c87e4bf

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/Algebra/Construct/Quotient/Group.agda

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,9 @@ quotientIsGroup = record
105105
quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
106106
quotientGroup = record { isGroup = quotientIsGroup }
107107

108+
_/_ : Group c (c ⊔ ℓ ⊔ c′)
109+
_/_ = quotientGroup
110+
108111
project : Group.Carrier G Group.Carrier quotientGroup
109112
project x = x -- because we do all the work in the relation
110113

0 commit comments

Comments
 (0)