Absolute values #
This file defines a bundled type of absolute values AbsoluteValue R S
.
Main definitions #
AbsoluteValue R S
is the type of absolute values onR
mapping toS
.AbsoluteValue.abs
is the "standard" absolute value onS
, mapping negativex
to-x
.AbsoluteValue.toMonoidWithZeroHom
: absolute values mapping to a linear ordered field preserve0
,*
and1
IsAbsoluteValue
: a type class stating thatf : β → α
satisfies the axioms of an absolute value
AbsoluteValue R S
is the type of absolute values on R
mapping to S
:
the maps that preserve *
, are nonnegative, positive definite and satisfy
the triangle inequality.
- toFun : R → S
The absolute value is nonnegative
The absolute value is positive definitive
The absolute value satisfies the triangle inequality
Instances For
Equations
See Note [custom simps projection].
Equations
Instances For
The triangle inequality for an AbsoluteValue
applied to a list.
Alias of the reverse direction of AbsoluteValue.ne_zero_iff
.
Alias of the reverse direction of AbsoluteValue.pos_iff
.
Absolute values from a nontrivial R
to a linear ordered ring preserve *
, 0
and 1
.
Equations
Instances For
Absolute values from a nontrivial R
to a linear ordered ring preserve *
and 1
.
Equations
Instances For
An absolute value satisfies f (n : R) ≤ n
for every n : ℕ
.
Bound abv (a + b)
from below
Bound abv (a - b)
from above
Values of an absolute value coincide on the image of ℕ
in R
if and only if they coincide on the image of ℤ
in R
.
AbsoluteValue.abs
is abs
as a bundled AbsoluteValue
.
Equations
Instances For
Equations
The trivial absolute value takes the value 1
on all nonzero elements.
Equations
Instances For
An absolute value on a semiring R
without zero divisors is nontrivial if it takes
a value ≠ 1
on a nonzero element.
This has the advantage over v ≠ .trivial
that it does not require decidability
of · = 0
in R
.
Equations
Instances For
A function f
is an absolute value if it is nonnegative, zero only at 0, additive, and
multiplicative.
See also the type AbsoluteValue
which represents a bundled version of absolute values.
The absolute value is nonnegative
The absolute value is positive definitive
The absolute value satisfies the triangle inequality
The absolute value is multiplicative
Instances
A bundled absolute value is an absolute value.
Convert an unbundled IsAbsoluteValue
to a bundled AbsoluteValue
.
Equations
Instances For
abv
as a MonoidWithZeroHom
.
Equations
Instances For
An absolute value as a monoid with zero homomorphism, assuming the target is a semifield.