PartiallyInvertibleRing concept

Description

A partially invertible ring is a ring in which only part of the elements have a multiplicative inverse.

The partially invertible ring has been defined to be able to ease the definition of a field. Also it allows to categorise sets of vectors and matrices that are a ring but for which the 0-vector or 0-matrix is not the only vector or matrix that does not have an inverse.

For instance, the vectors equipped with the element-multiplication have no inverse for any vector that contains a 0.

Refinement of

Ring and MultiplicativePartiallyInvertibleMonoid

Notation

Definitions

Valid expressions

Expression semantics

Complexity guarantees

Invariants

Models

Notes