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.

Equations

• WithAbs.delabToAbs = Lean.PrettyPrinter.Delaborator.delabApp

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

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

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.

Equations

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

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

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

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)

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

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

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)

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

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' := ⋯ }

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

@[instance_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 := ⋯ }

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

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

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

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

@[instance_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 := ⋯ }

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

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

@[instance_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 { toFun := WithAbs.ofAbs, invFun := WithAbs.toAbs v, left_inv := ⋯, right_inv := ⋯ }

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

@[instance_reducible]

instance 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

Equations

• WithAbs.moduleLeft v = { toSMul := WithAbs.instSMul v, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_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 := ⋯ }

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 = AddEquiv.linearEquiv R (WithAbs.equiv v).toAddEquiv

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

@[instance_reducible]

instance 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

Equations

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

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)

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

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

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

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

def AbsoluteValue.under {L : Type u_3} (K : Type u_4) {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (w : AbsoluteValue L S) : AbsoluteValue K S

The restriction of an absolute value w on L to K.

Equations

• AbsoluteValue.under K w = w.comp ⋯

theorem AbsoluteValue.under_def {L : Type u_3} (K : Type u_4) {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (w : AbsoluteValue L S) : under K w = w.comp ⋯

@[simp]

theorem AbsoluteValue.under_apply {L : Type u_3} (K : Type u_4) {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (w : AbsoluteValue L S) (x : K) : (under K w) x = w ((algebraMap K L) x)

class AbsoluteValue.LiesOver {L : Type u_3} {K : Type u_4} {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [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.

• under_eq : under K w = v

theorem AbsoluteValue.liesOver_iff {L : Type u_3} {K : Type u_4} {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (w : AbsoluteValue L S) (v : AbsoluteValue K S) : w.LiesOver v ↔ under K w = v

@[deprecated AbsoluteValue.LiesOver.under_eq (since := "2026-08-08")]

theorem AbsoluteValue.LiesOver.comp_eq {L : Type u_3} {K : Type u_4} {S : Type u_5} {inst✝ : CommSemiring K} {inst✝¹ : Semiring L} {inst✝² : Algebra K L} {inst✝³ : FaithfulSMul K L} {inst✝⁴ : PartialOrder S} {inst✝⁵ : Semiring S} (w : AbsoluteValue L S) (v : AbsoluteValue K S) [self : w.LiesOver v] : under K w = v

Alias of AbsoluteValue.LiesOver.under_eq.

instance AbsoluteValue.instLiesOverUnder {L : Type u_3} {K : Type u_4} {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (w : AbsoluteValue L S) : w.LiesOver (under K w)

theorem AbsoluteValue.over_def {L : Type u_3} {K : Type u_4} {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (w : AbsoluteValue L S) (v : AbsoluteValue K S) [w.LiesOver v] : v = under K w

@[simp]

theorem AbsoluteValue.under_under {L : Type u_3} (K : Type u_4) {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (M : Type u_6) [CommSemiring M] [Algebra K M] [Algebra M L] [IsScalarTower K M L] [FaithfulSMul K M] [FaithfulSMul M L] (w : AbsoluteValue L S) : under K (under M w) = under K w

@[simp]

theorem AbsoluteValue.under_liesOver_iff {L : Type u_3} {K : Type u_4} {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] (M : Type u_6) [CommSemiring M] [Algebra K M] [Algebra M L] [IsScalarTower K M L] [FaithfulSMul K M] [FaithfulSMul M L] {w : AbsoluteValue L S} {v : AbsoluteValue K S} : (under M w).LiesOver v ↔ w.LiesOver v

theorem AbsoluteValue.LiesOver.trans {L : Type u_3} {K : Type u_4} {S : Type u_5} [CommSemiring K] [Semiring L] [Algebra K L] [FaithfulSMul K L] [PartialOrder S] [Semiring S] {M : Type u_6} [CommSemiring M] [Algebra K M] [Algebra M L] [IsScalarTower K M L] [FaithfulSMul K M] [FaithfulSMul M L] (v : AbsoluteValue K S) (u : AbsoluteValue M S) (w : AbsoluteValue L S) [w.LiesOver u] [u.LiesOver v] : w.LiesOver v