Theorems · Inductive type · functional analysis

WithAbs

{R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : 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.

Defined in

Mathlib.Analysis.Normed.Ring.WithAbs

Cited by

102 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

SemiringPartialOrderSemiring