## `Ax::closedUnitNormals` -- the axiom of closed unit normals

#### Introduction

`Ax::closedUnitNormals` states that the unit normals of an integral domain are closed under multiplication.

#### Generating the axiom

`Ax::closedUnitNormals()`

#### Details

- The axiom `Ax::closedUnitNormals` is used to state that the unit normals of an integral domain are closed under multiplication, i.e., that `dom::equal(x, dom::unitNormal(a) * dom::unitNormal(b)) = TRUE` implies `dom::equal(x, dom::unitNormal(x)) = TRUE` for all elements `x`, `a` and `b` of the domain `dom`.
- This axiom may be used only in conjunction with the axiom `Ax::canonicalUnitNormal`. If an integral domain has no unique unit normals, this axiom may not be stated.

#### Changes

- no changes

Do you have questions or comments?
Copyright © SciFace Software GmbH & Co. KG 2000