WithAbs type synonym

WithAbs v is a copy of the semiring R with the same underlying ring structure, but assigned v-dependent instances (such as NormedRing) where v is an absolute value on R.

Main definitions

• WithAbs : 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. This can be used to assign and infer instances on a semiring that depend on absolute values.
• WithAbs.equiv v : The canonical ring equivalence between WithAbs v and R.

structure WithAbs {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : 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.

• toAbs :: (
• ofAbs : R

  Converts an element of WithAbs v to an element of R.

• )

def WithAbs.delabToAbs : Lean.PrettyPrinter.Delaborator.Delab

This prevents toAbs p x being printed as { ofAbs := x } by delabStructureInstance.

@[implicit_reducible]

instance WithAbs.instSemiring {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Semiring (WithAbs v)

theorem WithAbs.ofAbs_toAbs {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x : R) : (toAbs v x).ofAbs = x

@[simp]

theorem WithAbs.toAbs_ofAbs {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x : WithAbs v) : toAbs v x.ofAbs = x

theorem WithAbs.ofAbs_surjective {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Function.Surjective ofAbs

theorem WithAbs.toAbs_surjective {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Function.Surjective (toAbs v)

theorem WithAbs.ofAbs_injective {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Function.Injective ofAbs

theorem WithAbs.toAbs_injective {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Function.Injective (toAbs v)

theorem WithAbs.ofAbs_bijective {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Function.Bijective ofAbs

theorem WithAbs.toAbs_bijective {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Function.Bijective (toAbs v)

@[simp]

theorem WithAbs.toAbs_zero {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : toAbs v 0 = 0

@[simp]

theorem WithAbs.ofAbs_zero {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : ofAbs 0 = 0

@[simp]

theorem WithAbs.toAbs_one {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : toAbs v 1 = 1

@[simp]

theorem WithAbs.ofAbs_one {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : ofAbs 1 = 1

@[simp]

theorem WithAbs.toAbs_add {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x y : R) : toAbs v (x + y) = toAbs v x + toAbs v y

@[simp]

theorem WithAbs.ofAbs_add {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x y : WithAbs v) : (x + y).ofAbs = x.ofAbs + y.ofAbs

@[simp]

theorem WithAbs.toAbs_mul {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x y : R) : toAbs v (x * y) = toAbs v x * toAbs v y

@[simp]

theorem WithAbs.ofAbs_mul {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x y : WithAbs v) : (x * y).ofAbs = x.ofAbs * y.ofAbs

@[simp]

theorem WithAbs.toAbs_eq_zero {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {x : R} : toAbs v x = 0 ↔ x = 0

@[simp]

theorem WithAbs.ofAbs_eq_zero {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {x : WithAbs v} : x.ofAbs = 0 ↔ x = 0

@[simp]

theorem WithAbs.toAbs_pow {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x : R) (n : ℕ) : toAbs v (x ^ n) = toAbs v x ^ n

@[simp]

theorem WithAbs.ofAbs_pow {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (x : WithAbs v) (n : ℕ) : (x ^ n).ofAbs = x.ofAbs ^ n

def WithAbs.equiv {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : WithAbs v ≃+* R

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

@[simp]

theorem WithAbs.equiv_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (self : WithAbs v) : (equiv v) self = self.ofAbs

@[simp]

theorem WithAbs.equiv_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) (ofAbs : R) : (equiv v).symm ofAbs = toAbs v ofAbs

instance WithAbs.instNontrivial {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) [Nontrivial R] : Nontrivial (WithAbs v)

@[implicit_reducible]

instance WithAbs.instUnique {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) [Unique R] : Unique (WithAbs v)

@[implicit_reducible]

instance WithAbs.instInhabited {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : Inhabited (WithAbs v)

def WithAbs.map {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} [Semiring T] (w : AbsoluteValue T S) (f : R →+* T) : WithAbs v →+* WithAbs w

Lift a ring hom to WithAbs.

@[simp]

theorem WithAbs.map_id {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : map v v (RingHom.id R) = RingHom.id (WithAbs v)

theorem WithAbs.map_comp {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} {U : Type u_4} [Semiring T] [Semiring U] (w : AbsoluteValue T S) (u : AbsoluteValue U S) (f : R →+* T) (g : T →+* U) : map v u (g.comp f) = (map w u g).comp (map v w f)

@[simp]

theorem WithAbs.map_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} [Semiring T] (w : AbsoluteValue T S) (f : R →+* T) (x : WithAbs v) : (map v w f) x = toAbs w (f x.ofAbs)

def WithAbs.congr {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} [Semiring T] (w : AbsoluteValue T S) (f : R ≃+* T) : WithAbs v ≃+* WithAbs w

Lift a RingEquiv to WithAbs.

@[simp]

theorem WithAbs.congr_refl {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) : congr v v (RingEquiv.refl R) = RingEquiv.refl (WithAbs v)

theorem WithAbs.congr_trans {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} {U : Type u_4} [Semiring T] [Semiring U] (w : AbsoluteValue T S) (u : AbsoluteValue U S) (f : R ≃+* T) (g : T ≃+* U) : congr v u (f.trans g) = (congr v w f).trans (congr w u g)

theorem WithAbs.congr_symm {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} [Semiring T] (w : AbsoluteValue T S) (f : R ≃+* T) : (congr v w f).symm = congr w v f.symm

@[simp]

theorem WithAbs.congr_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} [Semiring T] (w : AbsoluteValue T S) (f : R ≃+* T) (x : WithAbs v) : (congr v w f) x = toAbs w (f x.ofAbs)

@[simp]

theorem WithAbs.congr_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v : AbsoluteValue R S) {T : Type u_3} [Semiring T] (w : AbsoluteValue T S) (f : R ≃+* T) (x : WithAbs w) : (congr v w f).symm x = toAbs v (f.symm x.ofAbs)

@[deprecated "Use `WithAbs.congr` instead." (since := "2026-03-02")]

def WithAbs.equivWithAbs {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v w : AbsoluteValue R S) : WithAbs v ≃+* WithAbs w

The canonical (semiring) equivalence between WithAbs v and WithAbs w, for any two absolute values v and w on R.

@[deprecated "Use `WithAbs.congr_symm` instead." (since := "2026-03-02")]

theorem WithAbs.equivWithAbs_symm {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] (v w : AbsoluteValue R S) : (congr v w (RingEquiv.refl R)).symm = congr w v (RingEquiv.refl R).symm

@[deprecated "Use `simp`." (since := "2026-03-02")]

theorem WithAbs.equiv_equivWithAbs_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] {v w : AbsoluteValue R S} {x : WithAbs w} : (equiv v) ((congr v w (RingEquiv.refl R)).symm x) = (equiv w) x

@[deprecated "Use `simp`." (since := "2026-03-02")]

theorem WithAbs.equivWithAbs_equiv_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] {v w : AbsoluteValue R S} {x : R} : (congr v w (RingEquiv.refl R)) ((equiv v).symm x) = (equiv w).symm x

@[deprecated "Use `simp`." (since := "2026-03-02")]

theorem WithAbs.equivWithAbs_symm_equiv_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Semiring R] {v w : AbsoluteValue R S} {x : R} : (congr v w (RingEquiv.refl R)).symm ((equiv w).symm x) = (equiv v).symm x

@[implicit_reducible]

instance WithAbs.instCommSemiring {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [CommSemiring R] (v : AbsoluteValue R S) : CommSemiring (WithAbs v)

@[implicit_reducible]

instance WithAbs.instRing {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Ring R] (v : AbsoluteValue R S) : Ring (WithAbs v)

@[implicit_reducible]

noncomputable instance WithAbs.normedRing {R : Type u_1} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing (WithAbs v)

theorem WithAbs.norm_eq_apply_ofAbs {R : Type u_1} [Ring R] (v : AbsoluteValue R ℝ) (x : WithAbs v) : ‖x‖ = v x.ofAbs

theorem WithAbs.norm_toAbs_eq {R : Type u_1} [Ring R] (v : AbsoluteValue R ℝ) (x : R) : ‖toAbs v x‖ = v x

@[deprecated WithAbs.norm_eq_apply_ofAbs (since := "2026-03-02")]

theorem WithAbs.norm_eq_abv {R : Type u_1} [Ring R] (v : AbsoluteValue R ℝ) (x : WithAbs v) : ‖x‖ = v x.ofAbs

Alias of WithAbs.norm_eq_apply_ofAbs.

@[deprecated WithAbs.norm_toAbs_eq (since := "2026-03-02")]

theorem WithAbs.norm_eq_abv' {R : Type u_1} [Ring R] (v : AbsoluteValue R ℝ) (x : R) : ‖toAbs v x‖ = v x

Alias of WithAbs.norm_toAbs_eq.

@[simp]

theorem WithAbs.toAbs_sub {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Ring R] (v : AbsoluteValue R S) (x y : R) : toAbs v (x - y) = toAbs v x - toAbs v y

@[simp]

theorem WithAbs.ofAbs_sub {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Ring R] (v : AbsoluteValue R S) (x y : WithAbs v) : (x - y).ofAbs = x.ofAbs - y.ofAbs

@[simp]

theorem WithAbs.toAbs_neg {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Ring R] (v : AbsoluteValue R S) (x : R) : toAbs v (-x) = -toAbs v x

@[simp]

theorem WithAbs.ofAbs_neg {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [Ring R] (v : AbsoluteValue R S) (x : WithAbs v) : (-x).ofAbs = -x.ofAbs

@[implicit_reducible]

instance WithAbs.instCommRing {R : Type u_1} {S : Type u_2} [Semiring S] [PartialOrder S] [CommRing R] (v : AbsoluteValue R S) : CommRing (WithAbs v)

@[implicit_reducible]

instance WithAbs.instSMul {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [SMul R T] : SMul (WithAbs v) T

theorem WithAbs.smul_left_def {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [SMul R T] (x : WithAbs v) (t : T) : x • t = x.ofAbs • t

instance WithAbs.instFaithfulSMul {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [SMul R T] [FaithfulSMul R T] : FaithfulSMul (WithAbs v) T

@[implicit_reducible]

instance WithAbs.instSMul_1 {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [SMul T R] : SMul T (WithAbs v)

theorem WithAbs.smul_right_def {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [SMul T R] (t : T) (x : WithAbs v) : t • x = toAbs v (t • x.ofAbs)

instance WithAbs.instFaithfulSMul_1 {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [SMul T R] [FaithfulSMul T R] : FaithfulSMul T (WithAbs v)

instance WithAbs.instIsScalarTower {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) {P : Type u_5} [SMul T P] [SMul R T] [SMul R P] [IsScalarTower R T P] : IsScalarTower (WithAbs v) T P

instance WithAbs.instIsScalarTower_1 {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) {P : Type u_5} [SMul P R] [SMul T R] [SMul P T] [IsScalarTower P T R] : IsScalarTower P T (WithAbs v)

instance WithAbs.instIsScalarTower_2 {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) {P : Type u_5} [SMul P R] [SMul P T] [SMul R T] [IsScalarTower P R T] : IsScalarTower P (WithAbs v) T

@[implicit_reducible]

def WithAbs.moduleLeft {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [AddCommMonoid T] [Module R T] : Module (WithAbs v) T

Not an instance because it causes non-reducible diamonds when T = WithAbs v.

@[deprecated WithAbs.moduleLeft (since := "2026-03-02")]

def WithAbs.instModule_left {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [AddCommMonoid T] [Module R T] : Module (WithAbs v) T

Alias of WithAbs.moduleLeft.

---

Not an instance because it causes non-reducible diamonds when T = WithAbs v.

@[implicit_reducible]

instance WithAbs.instModule {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [Semiring T] [Module T R] : Module T (WithAbs v)

@[deprecated WithAbs.instModule (since := "2026-03-02")]

def WithAbs.instModule_right {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] (v : AbsoluteValue R S) [Semiring T] [Module T R] : Module T (WithAbs v)

Alias of WithAbs.instModule.

def WithAbs.linearEquiv {S : Type u_2} [Semiring S] [PartialOrder S] (R : Type u_3) {T : Type u_4} [Semiring R] [Semiring T] [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.

@[simp]

theorem WithAbs.linearEquiv_apply {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] [Semiring T] [Module R T] {v : AbsoluteValue T S} (x : WithAbs v) : (linearEquiv R v) x = x.ofAbs

@[simp]

theorem WithAbs.linearEquiv_symm_apply {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [Semiring R] [Semiring T] [Module R T] {v : AbsoluteValue T S} (x : T) : (linearEquiv R v).symm x = toAbs v x

@[implicit_reducible]

def WithAbs.algebraLeft {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} (T : Type u_4) [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue R S) : Algebra (WithAbs v) T

Not an instance because it causes non-reducible diamonds when T = WithAbs v.

theorem WithAbs.algebraMap_left_apply {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] {v : AbsoluteValue R S} (x : WithAbs v) : (algebraMap (WithAbs v) T) x = (algebraMap R T) x.ofAbs

theorem WithAbs.algebraMap_left_injective {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue R S) (h : Function.Injective ⇑(algebraMap R T)) : Function.Injective ⇑(algebraMap (WithAbs v) T)

@[implicit_reducible]

instance WithAbs.instAlgebra {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue T S) : Algebra R (WithAbs v)

theorem WithAbs.algebraMap_right_apply {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] {v : AbsoluteValue T S} (x : R) : (algebraMap R (WithAbs v)) x = toAbs v ((algebraMap R T) x)

theorem WithAbs.algebraMap_right_injective {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue T S) (h : Function.Injective ⇑(algebraMap R T)) : Function.Injective ⇑(algebraMap R (WithAbs v))

theorem WithAbs.ofAbs_algebraMap {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue R S) (w : AbsoluteValue T S) (x : WithAbs v) : ((algebraMap (WithAbs v) (WithAbs w)) x).ofAbs = (algebraMap R T) x.ofAbs

@[deprecated WithAbs.algebraLeft (since := "2026-03-02")]

def WithAbs.instAlgebra_left {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} (T : Type u_4) [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue R S) : Algebra (WithAbs v) T

Alias of WithAbs.algebraLeft.

---

Not an instance because it causes non-reducible diamonds when T = WithAbs v.

@[deprecated WithAbs.instAlgebra (since := "2026-03-02")]

def WithAbs.instAlgebra_right {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue T S) : Algebra R (WithAbs v)

Alias of WithAbs.instAlgebra.

def WithAbs.algEquiv {S : Type u_2} [Semiring S] [PartialOrder S] (R : Type u_3) {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue T S) : WithAbs v ≃ₐ[R] T

The canonical algebra isomorphism from an R-algebra R' with an absolute value v to R'.

@[simp]

theorem WithAbs.algEquiv_apply {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue T S) (x : WithAbs v) : (algEquiv R v) x = x.ofAbs

@[simp]

theorem WithAbs.algEquiv_symm_apply {S : Type u_2} [Semiring S] [PartialOrder S] {R : Type u_3} {T : Type u_4} [CommSemiring R] [Semiring T] [Algebra R T] (v : AbsoluteValue T S) (x : T) : (algEquiv R v).symm x = toAbs v x

class AbsoluteValue.LiesOver {K : Type u_3} {L : Type u_4} {S : Type u_5} [CommRing K] [IsSimpleRing K] [CommRing L] [Algebra K L] [PartialOrder S] [Nontrivial L] [Semiring S] (w : AbsoluteValue L S) (v : AbsoluteValue K S) : Prop

An absolute value w of L / K lies over the absolute value v of K if v is the restriction of w to K.

• comp_eq : w.comp ⋯ = v