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 MultiplicativeGroup
for the whole set without 0.
Refinement of
CommutativeRing
Notation
Definitions
Valid expressions
The expressions from CommutativeRing and:
Name |
Expression |
Return type |
Division |
a / b |
X |
Division assignment |
a /= b |
X |
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