Theorems · Definition · functional analysis

WithAbs.equiv

{R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] → [inst_1 : PartialOrder S] → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → WithAbs v ≃+* R

The canonical (semiring) equivalence between WithAbs v and R.

Defined in: Mathlib.Analysis.Normed.Ring.WithAbs
Cited by: 15 results in Mathlib
Foundations: Depth 26 from the axioms · uses propext, Quot.sound
Assumes: Semiring PartialOrder Semiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
PartialOrderstatement and proof · cited by 6,410
RingEquivstatement · cited by 1,147
AbsoluteValuestatement and proof · cited by 363
WithAbsstatement · cited by 102
WithAbs.ofAbsproof · cited by 35

Cited by18

Results whose statement or proof uses this declaration.

WithAbs.equiv_applystatement and proof · cited by 8
NumberField.InfinitePlace.Completion.extensionEmbedding_coestatement · cited by 5
WithAbs.equiv_symm_applystatement and proof · cited by 5
WithAbs.mapproof · cited by 3
WithAbs.linearEquivproof · cited by 2
NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coestatement · cited by 2
WithAbs.algEquivproof · cited by 2
NumberField.InfinitePlace.isometry_embeddingstatement and proof · cited by 2
NumberField.InfinitePlace.isometry_embedding_of_isRealstatement and proof · cited by 2
NumberField.InfinitePlace.Completion.WithAbs.ratCast_equivstatement and proof · cited by 1
AbsoluteValue.denseRange_algebraMap_piproof · cited by 1
NumberField.InfinitePlace.Completion.norm_coestatement · cited by 1