Field concept
Description
A field is a
CommutativeRing
where 0 is different from 1 and
each element a≠0 has the inverse 1/a.
Hence, a field is a
AdditiveAbelianGroup
and a MultiplicativePartiallyInvertibleCommutativeMonoid where only 0 has no multiplicative inverse.
This implies that if the set S is a field then S\{0} is an
MultiplicativeAbelianGroup.
Refinement of
CommutativeRing,
AdditiveAbelianGroup and
MultiplicativePartiallyInvertibleCommutativeMonoid.
Notation
| S
| Type of set |
| a,b
| Object of type S |
Definitions
Valid expressions
The expressions from CommutativeRing and:
| Name |
Expression |
Return type |
| Division |
a / b |
S |
| Division assignment |
a /= b |
S |
Expression semantics
| Name |
Expression |
Precondition |
Semantics |
Postcondition |
| Division |
a / b |
b≠0 |
equivalent to a = a * (1/b) |
|
| Division assignment |
a /= b |
b≠0 |
equivalent to a = a / b |
|
Complexity guarantees
Invariants
The invariants of
CommutativeRing and:
| Inversion |
for a≠0 we have a / a = 1 |
Models
Notes
- The set {0} with 0+0=0 and 0*0=0 fulfills all requirements of a field.
As this field does not provide practical usage we exclude it from our
considerations.
Allowing 0=1 in a set implies that this set is {0}. For this reason
we require 0≠1 in the description.