We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent cac627b commit e9dc02fCopy full SHA for e9dc02f
src/Algebra/Definitions.agda
@@ -50,7 +50,8 @@ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
50
Commutative : Op₂ A → Set _
51
Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
52
53
--- An element is called `Central` for a binary operation if it commutes with all other elements.
+-- An element is called `Central` for a binary operation
54
+-- if it commutes with all other elements.
55
Central : Op₂ A → A → Set _
56
Central _∙_ x = ∀ y → (x ∙ y) ≈ (y ∙ x)
57
0 commit comments