`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.

source

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.

)

Instances For

source

def WithAbs.delabToAbs :

Lean.PrettyPrinter.Delaborator.Delab

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

Equations

WithAbs.delabToAbs = Lean.PrettyPrinter.Delaborator.delabApp

Instances For

source

@[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)

Equations

WithAbs.instSemiring v = { toFun := WithAbs.ofAbs, invFun := WithAbs.toAbs v, left_inv := ⋯, right_inv := ⋯ }.semiring

source

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

source

@[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

source

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

source

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)

source

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

source

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)

source

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

source

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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

WithAbs.equiv v = { toFun := WithAbs.ofAbs, invFun := WithAbs.toAbs v, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[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

source

@[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

source

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)

source

@[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)

Equations

WithAbs.instUnique v = (WithAbs.equiv v).unique

source

@[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)

Equations

WithAbs.instInhabited v = { default := 0 }

source

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.

Equations

WithAbs.map v w f = (WithAbs.equiv w).symm.toRingHom.comp (f.comp (WithAbs.equiv v).toRingHom)

Instances For

source

@[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)

source

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)

source

@[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)

source

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.

Equations

WithAbs.congr v w f = { toFun := (↑↑(WithAbs.map v w f.toRingHom)).toFun, invFun := ⇑(WithAbs.map w v f.symm.toRingHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[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)

source

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)

source

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

source

@[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)

source

@[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)

source

@[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.

Equations

WithAbs.equivWithAbs v w = WithAbs.congr v w (RingEquiv.refl R)

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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)

Equations

WithAbs.instCommSemiring v = { toSemiring := WithAbs.instSemiring v, mul_comm := ⋯ }

source

@[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)

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

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

NormedRing (WithAbs v)

Equations

One or more equations did not get rendered due to their size.

source

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

‖x‖ = v x.ofAbs

source

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

‖toAbs v x‖ = v x

source

@[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.

source

@[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.

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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)

Equations

WithAbs.instCommRing v = { toRing := WithAbs.instRing v, mul_comm := ⋯ }

source

@[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

Equations

WithAbs.instSMul v = { smul := fun (x : WithAbs v) (t : T) => x.ofAbs • t }

source

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

source

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

source

@[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)

Equations

WithAbs.instSMul_1 v = Equiv.smul T (WithAbs.equiv v).toEquiv

source

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)

source

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)

source

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

source

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)

source

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

source

@[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.

Equations

WithAbs.moduleLeft v = Module.compHom T (WithAbs.equiv v).toRingHom

Instances For

source

@[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.

Equations

@WithAbs.instModule_left = @WithAbs.moduleLeft

Instances For

source

@[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)

Equations

WithAbs.instModule v = { toSMul := WithAbs.instSMul_1 v, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source

@[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.

Equations

@WithAbs.instModule_right = @WithAbs.instModule

Instances For

source

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.

Equations

WithAbs.linearEquiv R v = Equiv.linearEquiv R (WithAbs.equiv v).toEquiv

Instances For

source

@[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

source

@[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

source

@[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.

Equations

WithAbs.algebraLeft T v = Algebra.compHom T (WithAbs.equiv v).toRingHom

Instances For

source

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

source

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)

source

@[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)

Equations

One or more equations did not get rendered due to their size.

source

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)

source

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))

source

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

source

@[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.

Equations

@WithAbs.instAlgebra_left = @WithAbs.algebraLeft

Instances For

source

@[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.

Equations

@WithAbs.instAlgebra_right = @WithAbs.instAlgebra

Instances For

source

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'.

Equations

WithAbs.algEquiv R v = Equiv.algEquiv R (WithAbs.equiv v).toEquiv

Instances For

source

@[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

source

@[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

source

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

Instances

Documentation

Mathlib.Analysis.Normed.Ring.WithAbs

`WithAbs` type synonym #

Main definitions #

WithAbs type synonym #

Main definitions #

`WithAbs` type synonym #