Ax::closedUnitNormals
-- the axiom of closed unit normalsAx::closedUnitNormals
states that the unit normals of
an integral domain are closed under multiplication.
Ax::closedUnitNormals()
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
.Ax::canonicalUnitNormal
. If
an integral domain has no unique unit normals, this axiom may not be
stated.