From e65e6938bf0b440d7d6ae75acbb58bf3955f7437 Mon Sep 17 00:00:00 2001 From: Artem Korsakov Date: Sat, 4 Jul 2026 12:25:56 +0300 Subject: [PATCH 1/2] Update jump_start_guide.md --- docs/algebra.md | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/docs/algebra.md b/docs/algebra.md index 7e4972284e..211b710eef 100644 --- a/docs/algebra.md +++ b/docs/algebra.md @@ -47,18 +47,21 @@ The `algebra.ring` package contains more sophisticated structures which combine All ring-like structures are associative for both `+` and `*`, have commutative `+`, and have a `zero` element (an identity for `+`). -|Name |Has `negate`?|Has `1`?|Has `reciprocal`?|Commutative `*`?| -|--------------------|-------------|--------|-----------------|----------------| -|Semiring | | | | | -|Rng | ✓| | | | -|Rig | | ✓| | | -|CommutativeRig | | ✓| | ✓| -|Ring | ✓| ✓| | | -|CommutativeRing | ✓| ✓| | ✓| -|Semifield | | ✓| ✓| | -|CommutativeSemifield| | ✓| ✓| ✓| -|Field | ✓| ✓| ✓| ✓| - +| Name | Has `negate`? | Has `1`? | Has `reciprocal`? | Commutative `*`? | Has `gcd`/`lcm`? | Has `quot`/`mod`? | +|----------------------|----------------|-----------|--------------------|-------------------|-------------------|--------------------| +| Semiring | | | | | | | +| Rng | ✓ | | | | | | +| Rig | | ✓ | | | | | +| CommutativeSemiring | | | | ✓ | | | +| CommutativeRng | ✓ | | | ✓ | | | +| CommutativeRig | | ✓ | | ✓ | | | +| Ring | ✓ | ✓ | | | | | +| CommutativeRing | ✓ | ✓ | | ✓ | | | +| Semifield | | ✓ | ✓ | | | | +| CommutativeSemifield | | ✓ | ✓ | ✓ | | | +| GCDRing | ✓ | ✓ | | ✓ | ✓ | | +| EuclideanRing | ✓ | ✓ | | ✓ | ✓ | ✓ | +| Field | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | (For a description of what the terminology in each column means, see [§algebraic properties and terminology](#algebraic-properties-and-terminology).) From bdb2130d817936043ab05e74e2bdc1291b8464ce Mon Sep 17 00:00:00 2001 From: Artem Korsakov Date: Sun, 5 Jul 2026 12:28:24 +0300 Subject: [PATCH 2/2] Update algebra.md --- docs/algebra.md | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/docs/algebra.md b/docs/algebra.md index 211b710eef..27018464a1 100644 --- a/docs/algebra.md +++ b/docs/algebra.md @@ -91,18 +91,19 @@ The law of the excluded middle can be expressed as: - `(a ∨ (a → 0))` = `1` -|Name |Has `join`?|Has `meet`?|Has `zero`?|Has `one`?|Distributive|Has `imp`?|Excludes middle?| -|--------------------------|-----------|-----------|-----------|----------|------------|----------|----------------| -|JoinSemilattice | ✓| | | | | | | -|MeetSemilattice | | ✓| | | | | | -|BoundedJoinSemilattice | ✓| | ✓| | | | | -|BoundedMeetSemilattice | | ✓| | ✓| | | | -|Lattice | ✓| ✓| | | | | | -|DistributiveLattice | ✓| ✓| | | ✓| | | -|BoundedLattice | ✓| ✓| ✓| ✓| | | | -|BoundedDistributiveLattice| ✓| ✓| ✓| ✓| ✓| | | -|Heyting | ✓| ✓| ✓| ✓| ✓| ✓| | -|Bool | ✓| ✓| ✓| ✓| ✓| ✓| ✓| +| Name | Has `join`? | Has `meet`? | Has `zero`? | Has `one`? | Distributive | Has `imp`? | Excludes middle? | +|----------------------------|-------------|-------------|-------------|------------|--------------|------------|------------------| +| JoinSemilattice | ✓ | | | | | | | +| MeetSemilattice | | ✓ | | | | | | +| BoundedJoinSemilattice | ✓ | | ✓ | | | | | +| BoundedMeetSemilattice | | ✓ | | ✓ | | | | +| Lattice | ✓ | ✓ | | | | | | +| DistributiveLattice | ✓ | ✓ | | | ✓ | | | +| BoundedLattice | ✓ | ✓ | ✓ | ✓ | | | | +| BoundedDistributiveLattice | ✓ | ✓ | ✓ | ✓ | ✓ | | | +| Heyting | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | | +| GenBool | ✓ | ✓ | ✓ | | ✓ | | | +| Bool | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | Note that a `BoundedDistributiveLattice` gives you a `CommutativeRig`, but not the other way around: rigs aren't distributive with `a + (b * c) = (a + b) * (a + c)`.