Skip to content

Commit cac627b

Browse files
Update src/Algebra/Definitions.agda
Co-authored-by: Jacques Carette <[email protected]>
1 parent 8038838 commit cac627b

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Algebra/Definitions.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
5050
Commutative : Op₂ A Set _
5151
Commutative _∙_ = x y (x ∙ y) ≈ (y ∙ x)
5252

53+
-- An element is called `Central` for a binary operation if it commutes with all other elements.
5354
Central : Op₂ A A Set _
5455
Central _∙_ x = y (x ∙ y) ≈ (y ∙ x)
5556

0 commit comments

Comments
 (0)