Skip to main content

Semiring

typeclass S: Semiring extends AddCommMonoid, Monoid {
    distrib_left(a: S, b: S, c: S) {
        a * (b + c) = (a * b) + (a * c)
    }
    distrib_right(a: S, b: S, c: S) {
        (a + b) * c = (a * c) + (b * c)
    }
    mul_zero_left(a: S) {
        a * S.0 = S.0
    }
    mul_zero_right(a: S) {
        S.0 * a = S.0
    }
}

A semiring is like a ring but without additive inverses. It has two operations where addition forms a commutative monoid, multiplication forms a monoid, and multiplication distributes over addition.

GitHub

add​

Inherited from Add.

add_associative​

Inherited from AddSemigroup.

add_commutative​

Inherited from AddCommSemigroup.

add_identity_left​

Inherited from AddMonoid.

add_identity_right​

Inherited from AddMonoid.

distrib_left​

distrib_left(a: S, b: S, c: S) {
    a * (b + c) = (a * b) + (a * c)
}

Multiplication distributes over addition from the left: a * (b + c) = (a * b) + (a * c).

distrib_right​

distrib_right(a: S, b: S, c: S) {
    (a + b) * c = (a * c) + (b * c)
}

Multiplication distributes over addition from the right: (a + b) * c = (a * c) + (b * c).

mul​

Inherited from Mul.

mul_associative​

Inherited from Semigroup.

mul_identity_left​

Inherited from Monoid.

mul_identity_right​

Inherited from Monoid.

mul_zero_left​

mul_zero_left(a: S) {
    a * S.0 = S.0
}

Multiplying by the additive identity yields the additive identity.

mul_zero_right​

mul_zero_right(a: S) {
    S.0 * a = S.0
}

Multiplying the additive identity by anything yields the additive identity.

pow​

Inherited from Monoid.