Theorems · Definition · functional analysis

WithAbs.linearEquiv

{S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      (R : Type u_3) →
        {T : Type u_4} →
          [inst_2 : Semiring R] →
            [inst_3 : Semiring T] → [inst_4 : Module R T] → (v : AbsoluteValue T S) → WithAbs v ≃ₗ[R] T

The canonical R-linear isomorphism between WithAbs v and T, when v : AbsoluteValue T S.

Defined in

Mathlib.Analysis.Normed.Ring.WithAbs

Cited by

2 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringPartialOrderSemiringSemiringModule