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