Skip to content

Commit 77ec62a

Browse files
Added missing CHANGELOG entry for #1020
1 parent da606bf commit 77ec62a

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

CHANGELOG.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,6 +220,11 @@ Other major additions
220220
Other minor additions
221221
---------------------
222222

223+
* Added new definition to `Algebra.Definitions`:
224+
```agda
225+
Interchangable _∘_ _∙_ = ∀ w x y z → ((w ∙ x) ∘ (y ∙ z)) ≈ ((w ∘ y) ∙ (x ∘ z))
226+
```
227+
223228
* Added new proofs to `Algebra.Properties.Group`:
224229
```agda
225230
⁻¹-injective : x ⁻¹ ≈ y ⁻¹ → x ≈ y

0 commit comments

Comments
 (0)