File tree Expand file tree Collapse file tree 1 file changed +0
-22
lines changed Expand file tree Collapse file tree 1 file changed +0
-22
lines changed Original file line number Diff line number Diff line change @@ -288,28 +288,6 @@ Additions to existing modules
288
288
uv≈wx⇒yu∙vz≈yw∙xz : (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
289
289
```
290
290
291
- * In ` Algebra.Properties.Semigroup ` adding consequences for associativity for semigroups
292
- ``` agda
293
- uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
294
- uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x
295
- uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
296
- uv≈w⇒x[uv∙y]≈x∙wy : ∀ x y → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y)
297
- uv≈w⇒[x∙yu]v≈x∙yw : ∀ x y → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w)
298
- uv≈w⇒[xu∙v]y≈x∙wy : ∀ x y → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y)
299
- uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w)
300
- uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y)
301
- uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z
302
- uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y))
303
- [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x)
304
- [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
305
- [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x)
306
- [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x))
307
- uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x)
308
- uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
309
- uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
310
- uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
311
- ```
312
-
313
291
* In ` Algebra.Properties.Semigroup.Divisibility ` :
314
292
``` agda
315
293
∣ˡ-trans : Transitive _∣ˡ_
You can’t perform that action at this time.
0 commit comments