Structures · Algebra
IsAbsoluteValue
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.
- Shape
- One type argument · adds abv_nonneg', abv_eq_zero', abv_add', abv_mul'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Real
- Rat
How is a type an instance?
Loading the hierarchy index…
Assumed by204
- CauSeq.Completion.Cauchy
- CauSeq.const
- CauSeq.lim
- CauSeq.equiv_lim
- CauSeq.Completion.ofRat
- IsAbsoluteValue.toAbsoluteValue
- IsAbsoluteValue.abv_add
- IsAbsoluteValue.abv_nonneg
- CauSeq.inv
- CauSeq.lim_eq_of_equiv_const
- IsAbsoluteValue.abv_mul
- CauSeq.lim_neg
- CauSeq.const_limZero
- CauSeq.abv_pos_of_not_limZero
- CauSeq.cauchy₃
- CauSeq.add_limZero
- CauSeq.lim_const
- CauSeq.cauchy₂
- CauSeq.lim_add
- IsAbsoluteValue.abv_sum
- CauSeq.mul_limZero_right
- IsAbsoluteValue.abv_zero
- CauSeq.neg_limZero
- CauSeq.mul_limZero_left
- IsAbsoluteValue.abv_pos
- CauSeq.const_equiv
- CauSeq.const_neg
- IsAbsoluteValue.abvHom
- CauSeq.sub_apply
- IsCauSeq.cauchy₂
- CauSeq.eq_lim_of_const_equiv
- IsAbsoluteValue.abv_sub
- CauSeq.Completion.mk_eq
- IsCauSeq.bounded
- Polynomial.tendsto_norm_atTop
- CauSeq.not_limZero_of_not_congr_zero
- CauSeq.const_sub
- IsCauSeq.cauchy₃
- Polynomial.isClosedMap_eval
- IsAbsoluteValue.abv_neg
- CauSeq.limZero_congr
- rat_mul_continuous_lemma
- IsCauSeq.of_abv_le
- Polynomial.tendsto_abv_eval₂_atTop
- IsCauSeq.bounded'
- CauSeq.bounded'
- IsAbsoluteValue.abvHom'
- CauSeq.const_apply
- CauSeq.zero_limZero
- CauSeq.const_add
Ancestors0
No ancestors.