WithAbs #
WithAbs v
is a type synonym for a semiring R
which depends on an absolute value. The point of
this is to allow the type class inference system to handle multiple sources of instances that
arise from absolute values.
Main definitions #
WithAbs
: type synonym for a semiring which depends on an absolute value. This is a function that takes an absolute value on a semiring and returns the semiring. This can be used to assign and infer instances on a semiring that depend on absolute values.WithAbs.equiv v
: the canonical (type) equivalence betweenWithAbs v
andR
.WithAbs.ringEquiv v
: The canonical ring equivalence betweenWithAbs v
andR
.
def
WithAbs
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[Semiring R]
:
AbsoluteValue R S → Type u_1
Type synonym for a semiring which depends on an absolute value. This is a function that takes an absolute value on a semiring and returns the semiring. We use this to assign and infer instances on a semiring that depend on absolute values.
This is also helpful when dealing with several absolute values on the same semiring.
Instances For
instance
WithAbs.instNontrivial
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[Semiring R]
(v : AbsoluteValue R S)
[Nontrivial R]
:
Nontrivial (WithAbs v)
instance
WithAbs.instUnique
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[Semiring R]
(v : AbsoluteValue R S)
[Unique R]
:
Equations
instance
WithAbs.instSemiring
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[Semiring R]
(v : AbsoluteValue R S)
:
Equations
instance
WithAbs.instInhabited
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[Semiring R]
(v : AbsoluteValue R S)
:
Equations
- WithAbs.instInhabited v = { default := 0 }
def
WithAbs.equiv
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[Semiring R]
(v : AbsoluteValue R S)
:
The canonical (semiring) equivalence between WithAbs v
and R
.
Equations
- WithAbs.equiv v = RingEquiv.refl (WithAbs v)
Instances For
instance
WithAbs.instCommSemiring
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[CommSemiring R]
(v : AbsoluteValue R S)
:
CommSemiring (WithAbs v)
Equations
instance
WithAbs.instRing
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[Ring R]
(v : AbsoluteValue R S)
:
Equations
- WithAbs.instRing v = inferInstanceAs (Ring R)
instance
WithAbs.instCommRing
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
[CommRing R]
(v : AbsoluteValue R S)
:
Equations
Equations
instance
WithAbs.instModule_left
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
{R' : Type u_3}
[Semiring R]
[AddCommGroup R']
[Module R R']
(v : AbsoluteValue R S)
:
Equations
- WithAbs.instModule_left v = inferInstanceAs (Module R R')
instance
WithAbs.instModule_right
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
{R' : Type u_3}
[Semiring R]
[Semiring R']
[Module R R']
(v : AbsoluteValue R' S)
:
Equations
- WithAbs.instModule_right v = inferInstanceAs (Module R R')
instance
WithAbs.instAlgebra_left
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
{R' : Type u_3}
[CommSemiring R]
[Semiring R']
[Algebra R R']
(v : AbsoluteValue R S)
:
Equations
- WithAbs.instAlgebra_left v = inferInstanceAs (Algebra R R')
instance
WithAbs.instAlgebra_right
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
{R' : Type u_3}
[CommSemiring R]
[Semiring R']
[Algebra R R']
(v : AbsoluteValue R' S)
:
Equations
- WithAbs.instAlgebra_right v = inferInstanceAs (Algebra R R')
def
WithAbs.algEquiv
{R : Type u_1}
{S : Type u_2}
[Semiring S]
[PartialOrder S]
{R' : Type u_3}
[CommSemiring R]
[Semiring R']
[Algebra R R']
(v : AbsoluteValue R' S)
:
The canonical algebra isomorphism from an R
-algebra R'
with an absolute value v
to R'
.