Ax::closedUnitNormals
-- the axiom of closed unit normals
IntroductionAx::closedUnitNormals states that the unit normals of
an integral domain are closed under multiplication.
Generating
the axiomAx::closedUnitNormals()
DetailsAx::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.