Ring concept

Description

A ring is a set of elements equipped with

and for which the addition and multiplication are distributive.

Refinement of

AdditiveAbelianGroup and MultiplicativeMonoid

Notation

S Type of a Set
a, b, c Objects of type S

Definitions

Valid expressions

Expression semantics

Complexity guarantees

Invariants

Pre-distributivity a * ( b + c ) = a*b + a*c
Post-distributivity (a + b ) * c = a*c + b*c

Models

Notes