naalgc.spad line 44 [edit on github]
MagmaWithUnit is the class of multiplicative monads with unit, i.e. sets with a binary operation and a unit element. Axioms leftIdentity("*":(%,%)->
%,1) 1*x=x rightIdentity("*":(%,%)->
%,1) x*1=x Common Additional Axioms unitsKnown---if "recip" says "failed", that PROVES input wasn't
a unit
1 returns the unit element, denoted by 1.
a^n
returns the n
-
th power of a
, defined by repeated squaring.
leftPower(a, n)
returns the n
-
th left power of a
, i.e. leftPower(a, n) := a * leftPower(a, n-1)
and leftPower(a, 0) := 1
.
leftRecip(a)
returns an element, which is a left inverse of a
, or "failed"
if such an element doesn't
exist or cannot be determined (see unitsKnown).
one?(a)
tests whether a
is the unit 1.
recip(a)
returns an element, which is both a left and a right inverse of a
, or "failed"
if such an element doesn't
exist or cannot be determined (see unitsKnown).
rightPower(a, n)
returns the n
-
th right power of a
, i.e. rightPower(a, n) := rightPower(a, n-1) * a
and rightPower(a, 0) := 1
.
rightRecip(a)
returns an element, which is a right inverse of a
, or "failed"
if such an element doesn't
exist or cannot be determined (see unitsKnown).
sample yields
a value of type %