Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro, Anne Baanen

! This file was ported from Lean 3 source module algebra.order.absolute_value
! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import Mathlib.Algebra.Order.Field.Defs
import Mathlib.Algebra.Order.Hom.Basic
import Mathlib.Algebra.Ring.Regular

/-!
# Absolute values

This file defines a bundled type of absolute values `AbsoluteValue R S`.

## Main definitions

* `AbsoluteValue R S` is the type of absolute values on `R` mapping to `S`.
* `AbsoluteValue.abs` is the "standard" absolute value on `S`, mapping negative `x` to `-x`.
* `AbsoluteValue.toMonoidWithZeroHom`: absolute values mapping to a
linear ordered field preserve `0`, `*` and `1`
* `IsAbsoluteValue`: a type class stating that `f : Ξ² β Ξ±` satisfies the axioms of an absolute
value
-/

/-- `AbsoluteValue R S` is the type of absolute values on `R` mapping to `S`:
the maps that preserve `*`, are nonnegative, positive definite and satisfy the triangle equality. -/
structure AbsoluteValue: {R : Type u_1} β
{S : Type u_2} β
[inst : Semiring R] β
[inst_1 : OrderedSemiring S] β
(toMulHom : R ββ* S) β
(β (x : R), 0 β€ MulHom.toFun toMulHom x) β
(β (x : R), MulHom.toFun toMulHom x = 0 β x = 0) β
(β (x y : R), MulHom.toFun toMulHom (x + y) β€ MulHom.toFun toMulHom x + MulHom.toFun toMulHom y) β
AbsoluteValue R SAbsoluteValue (R: Type ?u.2R S: Type ?u.5S : Type _: Type (?u.2+1)Type _) [Semiring: Type ?u.8 β Type ?u.8Semiring R: Type ?u.2R] [OrderedSemiring: Type ?u.11 β Type ?u.11OrderedSemiring S: Type ?u.5S] extends R: Type ?u.2R ββ* S: Type ?u.5S where
/-- The absolute value is nonnegative -/
nonneg': β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x : R),
0 β€ MulHom.toFun self.toMulHom xnonneg' : β x: ?m.348x, 0: ?m.3530 β€ toFun: R β StoFun x: ?m.348x
/-- The absolute value is positive definitive -/
eq_zero': β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x : R),
MulHom.toFun self.toMulHom x = 0 β x = 0eq_zero' : β x: ?m.652x, toFun: R β StoFun x: ?m.652x = 0: ?m.6570 β x: ?m.652x = 0: ?m.6750
/-- The absolute value satisfies the triangle inequality -/
add_le': β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x y : R),
MulHom.toFun self.toMulHom (x + y) β€ MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom yadd_le' : β x: ?m.851x y: ?m.854y, toFun: R β StoFun (x: ?m.851x + y: ?m.854y) β€ toFun: R β StoFun x: ?m.851x + toFun: R β StoFun y: ?m.854y
#align absolute_value AbsoluteValue: (R : Type u_1) β (S : Type u_2) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (maxu_1u_2)AbsoluteValue

namespace AbsoluteValue

-- Porting note: Removing nolints.
-- attribute [nolint doc_blame] AbsoluteValue.toMulHom

section OrderedSemiring

section Semiring

variable {R: Type ?u.15366R S: Type ?u.4874S : Type _: Type (?u.14362+1)Type _} [Semiring: Type ?u.3627 β Type ?u.3627Semiring R: Type ?u.1954R] [OrderedSemiring: Type ?u.7335 β Type ?u.7335OrderedSemiring S: Type ?u.3624S] (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.1967) β (S : Type ?u.1966) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.1967?u.1966)AbsoluteValue R: Type ?u.1954R S: Type ?u.1957S)

instance zeroHomClass: {R : Type u_1} β
{S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β ZeroHomClass (AbsoluteValue R S) R SzeroHomClass : ZeroHomClass: Type ?u.2022 β
(M : outParam (Type ?u.2021)) β
(N : outParam (Type ?u.2020)) β [inst : Zero M] β [inst : Zero N] β Type (max(max?u.2022?u.2021)?u.2020)ZeroHomClass (AbsoluteValue: (R : Type ?u.2024) β (S : Type ?u.2023) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.2024?u.2023)AbsoluteValue R: Type ?u.1987R S: Type ?u.1990S) R: Type ?u.1987R S: Type ?u.1990S where
coe f: ?m.2433f := f: ?m.2433f.toFun: {M : Type ?u.2446} β {N : Type ?u.2445} β [inst : Mul M] β [inst_1 : Mul N] β (M ββ* N) β M β NtoFun
coe_injective' f: ?m.2743f g: ?m.2746g h: ?m.2749h := byGoals accomplished! π
MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } (x + y) β€     MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } x +       MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } yh: (fun f => f.toFun)
{ toMulHom := { toFun := toFunβ, map_mul' := map_mul'β }, nonneg' := nonneg'β, eq_zero' := eq_zero'β,
add_le' := add_le'β } =   (fun f => f.toFun) gmk.mk{ toMulHom := { toFun := toFunβ, map_mul' := map_mul'β }, nonneg' := nonneg'β, eq_zero' := eq_zero'β,
MulHom.toFun { toFun := toFunβΒΉ, map_mul' := map_mul'βΒΉ } (x + y) β€     MulHom.toFun { toFun := toFunβΒΉ, map_mul' := map_mul'βΒΉ } x +       MulHom.toFun { toFun := toFunβΒΉ, map_mul' := map_mul'βΒΉ } ytoFunβ: R β Smap_mul'β: β (x y : R), toFunβ (x * y) = toFunβ x * toFunβ ynonneg'β: β (x : R), 0 β€ MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } xeq_zero'β: β (x : R), MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } x = 0 β x = 0add_le'β: β (x y : R),
MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } (x + y) β€     MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } x +       MulHom.toFun { toFun := toFunβ, map_mul' := map_mul'β } yh: (fun f => f.toFun)
{ toMulHom := { toFun := toFunβΒΉ, map_mul' := map_mul'βΒΉ }, nonneg' := nonneg'βΒΉ, eq_zero' := eq_zero'βΒΉ,
{ toMulHom := { toFun := toFunβ, map_mul' := map_mul'β }, nonneg' := nonneg'β, eq_zero' := eq_zero'β,
add_le' := add_le'β }mk.mk.mk.mk{ toMulHom := { toFun := toFunβΒΉ, map_mul' := map_mul'βΒΉ }, nonneg' := nonneg'βΒΉ, eq_zero' := eq_zero'βΒΉ,
add_le' := add_le'βΒΉ } =   { toMulHom := { toFun := toFunβ, map_mul' := map_mul'β }, nonneg' := nonneg'β, eq_zero' := eq_zero'β,
R: Type ?u.1987S: Type ?u.1990instβΒΉ: Semiring Rinstβ: OrderedSemiring Sabv, f, g: AbsoluteValue R Sh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gcongrGoals accomplished! π
map_zero f: ?m.2762f := (f: ?m.2762f.eq_zero': β {R : Type ?u.2765} {S : Type ?u.2764} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
(x : R), MulHom.toFun self.toMulHom x = 0 β x = 0eq_zero' _: ?m.2766_).2: β {a b : Prop}, (a β b) β b β a2 rfl: β {Ξ± : Sort ?u.2784} {a : Ξ±}, a = arfl
#align absolute_value.zero_hom_class AbsoluteValue.zeroHomClass: {R : Type u_1} β
{S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β ZeroHomClass (AbsoluteValue R S) R SAbsoluteValue.zeroHomClass

instance mulHomClass: MulHomClass (AbsoluteValue R S) R SmulHomClass : MulHomClass: Type ?u.3656 β
(M : outParam (Type ?u.3655)) β
(N : outParam (Type ?u.3654)) β [inst : Mul M] β [inst : Mul N] β Type (max(max?u.3656?u.3655)?u.3654)MulHomClass (AbsoluteValue: (R : Type ?u.3658) β (S : Type ?u.3657) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.3658?u.3657)AbsoluteValue R: Type ?u.3621R S: Type ?u.3624S) R: Type ?u.3621R S: Type ?u.3624S :=
{ AbsoluteValue.zeroHomClass: {R : Type ?u.4001} β
{S : Type ?u.4000} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β ZeroHomClass (AbsoluteValue R S) R SAbsoluteValue.zeroHomClass with map_mul := fun f: ?m.4709f => f: ?m.4709f.map_mul': β {M : Type ?u.4729} {N : Type ?u.4728} [inst : Mul M] [inst_1 : Mul N] (self : M ββ* N) (x y : M),
MulHom.toFun self (x * y) = MulHom.toFun self x * MulHom.toFun self ymap_mul' }
#align absolute_value.mul_hom_class AbsoluteValue.mulHomClass: {R : Type u_1} β
{S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β MulHomClass (AbsoluteValue R S) R SAbsoluteValue.mulHomClass

instance nonnegHomClass: {R : Type u_1} β
{S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β NonnegHomClass (AbsoluteValue R S) R SnonnegHomClass : NonnegHomClass: Type ?u.4906 β
outParam (Type ?u.4905) β
(Ξ² : outParam (Type ?u.4904)) β [inst : Zero Ξ²] β [inst : LE Ξ²] β Type (max(max?u.4906?u.4905)?u.4904)NonnegHomClass (AbsoluteValue: (R : Type ?u.4908) β (S : Type ?u.4907) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.4908?u.4907)AbsoluteValue R: Type ?u.4871R S: Type ?u.4874S) R: Type ?u.4871R S: Type ?u.4874S :=
{ AbsoluteValue.zeroHomClass: {R : Type ?u.5226} β
{S : Type ?u.5225} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β ZeroHomClass (AbsoluteValue R S) R SAbsoluteValue.zeroHomClass with map_nonneg := fun f: ?m.5776f => f: ?m.5776f.nonneg': β {R : Type ?u.5779} {S : Type ?u.5778} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
(x : R), 0 β€ MulHom.toFun self.toMulHom xnonneg' }
#align absolute_value.nonneg_hom_class AbsoluteValue.nonnegHomClass: {R : Type u_1} β
{S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β NonnegHomClass (AbsoluteValue R S) R SAbsoluteValue.nonnegHomClass

instance subadditiveHomClass: {R : Type u_1} β
{S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β SubadditiveHomClass (AbsoluteValue R S) R SsubadditiveHomClass : SubadditiveHomClass: Type ?u.5958 β
(Ξ± : outParam (Type ?u.5957)) β
(Ξ² : outParam (Type ?u.5956)) β
[inst : Add Ξ±] β [inst : Add Ξ²] β [inst : LE Ξ²] β Type (max(max?u.5958?u.5957)?u.5956)SubadditiveHomClass (AbsoluteValue: (R : Type ?u.5960) β (S : Type ?u.5959) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.5960?u.5959)AbsoluteValue R: Type ?u.5923R S: Type ?u.5926S) R: Type ?u.5923R S: Type ?u.5926S :=
{ AbsoluteValue.zeroHomClass: {R : Type ?u.6389} β
{S : Type ?u.6388} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β ZeroHomClass (AbsoluteValue R S) R SAbsoluteValue.zeroHomClass with map_add_le_add := fun f: ?m.7174f => f: ?m.7174f.add_le': β {R : Type ?u.7177} {S : Type ?u.7176} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
(x y : R), MulHom.toFun self.toMulHom (x + y) β€ MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom yadd_le' }
{S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β SubadditiveHomClass (AbsoluteValue R S) R SAbsoluteValue.subadditiveHomClass

@[simp]
theorem coe_mk: β (f : R ββ* S) {hβ : β (x : R), 0 β€ MulHom.toFun f x} {hβ : β (x : R), MulHom.toFun f x = 0 β x = 0}
{hβ : β (x y : R), MulHom.toFun f (x + y) β€ MulHom.toFun f x + MulHom.toFun f y},
β{ toMulHom := f, nonneg' := hβ, eq_zero' := hβ, add_le' := hβ } = βfcoe_mk (f: R ββ* Sf : R: Type ?u.7326R ββ* S: Type ?u.7329S) {hβ: β (x : R), 0 β€ MulHom.toFun f xhβ hβ: ?m.7691hβ hβ: ?m.7694hβ} : (AbsoluteValue.mk: {R : Type ?u.7702} β
{S : Type ?u.7701} β
[inst : Semiring R] β
[inst_1 : OrderedSemiring S] β
(toMulHom : R ββ* S) β
(β (x : R), 0 β€ MulHom.toFun toMulHom x) β
(β (x : R), MulHom.toFun toMulHom x = 0 β x = 0) β
(β (x y : R), MulHom.toFun toMulHom (x + y) β€ MulHom.toFun toMulHom x + MulHom.toFun toMulHom y) β
AbsoluteValue R SAbsoluteValue.mk f: R ββ* Sf hβ: ?m.7688hβ hβ: ?m.7691hβ hβ: ?m.7694hβ : R: Type ?u.7326R β S: Type ?u.7329S) = f: R ββ* Sf :=
rfl: β {Ξ± : Sort ?u.10678} {a : Ξ±}, a = arfl
#align absolute_value.coe_mk AbsoluteValue.coe_mk: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (f : R ββ* S)
{hβ : β (x : R), 0 β€ MulHom.toFun f x} {hβ : β (x : R), MulHom.toFun f x = 0 β x = 0}
{hβ : β (x y : R), MulHom.toFun f (x + y) β€ MulHom.toFun f x + MulHom.toFun f y},
β{ toMulHom := f, nonneg' := hβ, eq_zero' := hβ, add_le' := hβ } = βfAbsoluteValue.coe_mk

@[ext]
theorem ext: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] β¦f g : AbsoluteValue R Sβ¦,
(β (x : R), βf x = βg x) β f = gext β¦f: AbsoluteValue R Sf g: AbsoluteValue R Sg : AbsoluteValue: (R : Type ?u.10781) β
(S : Type ?u.10780) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.10781?u.10780)AbsoluteValue R: Type ?u.10747R S: Type ?u.10750Sβ¦ : (β x: ?m.10809x, f: AbsoluteValue R Sf x: ?m.10809x = g: AbsoluteValue R Sg x: ?m.10809x) β f: AbsoluteValue R Sf = g: AbsoluteValue R Sg :=
FunLike.ext: β {F : Sort ?u.11640} {Ξ± : Sort ?u.11641} {Ξ² : Ξ± β Sort ?u.11639} [i : FunLike F Ξ± Ξ²] (f g : F),
(β (x : Ξ±), βf x = βg x) β f = gFunLike.ext _: ?m.11642_ _: ?m.11642_
#align absolute_value.ext AbsoluteValue.ext: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] β¦f g : AbsoluteValue R Sβ¦,
(β (x : R), βf x = βg x) β f = gAbsoluteValue.ext

/-- See Note [custom simps projection]. -/
def Simps.apply: AbsoluteValue R S β R β SSimps.apply (f: AbsoluteValue R Sf : AbsoluteValue: (R : Type ?u.12111) β
(S : Type ?u.12110) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.12111?u.12110)AbsoluteValue R: Type ?u.12077R S: Type ?u.12080S) : R: Type ?u.12077R β S: Type ?u.12080S := f: AbsoluteValue R Sf
#align absolute_value.simps.apply AbsoluteValue.Simps.apply: {R : Type u_1} β {S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β AbsoluteValue R S β R β SAbsoluteValue.Simps.apply

initialize_simps_projections AbsoluteValue: (R : Type u_1) β (S : Type u_2) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (maxu_1u_2)AbsoluteValue (toFun: (R : Type u_1) β (S : Type u_2) β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β AbsoluteValue R S β R β StoFun β apply: {R : Type u_1} β {S : Type u_2} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β AbsoluteValue R S β R β Sapply)

-- Porting note:
-- These helper instances are unhelpful in Lean 4, so omitting:
-- /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
-- directly. -/
-- instance : CoeFun (AbsoluteValue R S) fun f => R β S :=
--   FunLike.hasCoeToFun

@[simp]
theorem coe_toMulHom: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
abv.toMulHom = βabvcoe_toMulHom : abv: AbsoluteValue R Sabv.toMulHom: {R : Type ?u.13173} β
{S : Type ?u.13172} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β AbsoluteValue R S β R ββ* StoMulHom = abv: AbsoluteValue R Sabv :=
rfl: β {Ξ± : Sort ?u.13420} {a : Ξ±}, a = arfl
#align absolute_value.coe_to_mul_hom AbsoluteValue.coe_toMulHom: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
abv.toMulHom = βabvAbsoluteValue.coe_toMulHom

protected theorem nonneg: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (x : R),
0 β€ βabv xnonneg (x: Rx : R: Type ?u.13446R) : 0: ?m.134830 β€ abv: AbsoluteValue R Sabv x: Rx :=
abv: AbsoluteValue R Sabv.nonneg': β {R : Type ?u.14324} {S : Type ?u.14323} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
(x : R), 0 β€ MulHom.toFun self.toMulHom xnonneg' x: Rx
#align absolute_value.nonneg AbsoluteValue.nonneg: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (x : R),
0 β€ βabv xAbsoluteValue.nonneg

@[simp]
protected theorem eq_zero: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
βabv x = 0 β x = 0eq_zero {x: Rx : R: Type ?u.14359R} : abv: AbsoluteValue R Sabv x: Rx = 0: ?m.148220 β x: Rx = 0: ?m.151030 :=
abv: AbsoluteValue R Sabv.eq_zero': β {R : Type ?u.15290} {S : Type ?u.15289} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
(x : R), MulHom.toFun self.toMulHom x = 0 β x = 0eq_zero' x: Rx
#align absolute_value.eq_zero AbsoluteValue.eq_zero: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
βabv x = 0 β x = 0AbsoluteValue.eq_zero

protected theorem add_le: β (x y : R), βabv (x + y) β€ βabv x + βabv yadd_le (x: Rx y: Ry : R: Type ?u.15366R) : abv: AbsoluteValue R Sabv (x: Rx + y: Ry) β€ abv: AbsoluteValue R Sabv x: Rx + abv: AbsoluteValue R Sabv y: Ry :=
abv: AbsoluteValue R Sabv.add_le': β {R : Type ?u.17450} {S : Type ?u.17449} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
(x y : R), MulHom.toFun self.toMulHom (x + y) β€ MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom yadd_le' x: Rx y: Ry
#align absolute_value.add_le AbsoluteValue.add_le: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (x y : R),
βabv (x + y) β€ βabv x + βabv yAbsoluteValue.add_le

-- Porting note: Removed since `map_mul` proves the theorem
--@[simp]
--protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y := map_mul _ _ _
--abv.map_mul' x y
#align absolute_value.map_mul map_mul: β {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N] (f : F)
(x y : M), βf (x * y) = βf x * βf ymap_mul

protected theorem ne_zero_iff: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
βabv x β  0 β x β  0ne_zero_iff {x: Rx : R: Type ?u.17490R} : abv: AbsoluteValue R Sabv x: Rx β  0: ?m.179550 β x: Rx β  0: ?m.182220 :=
abv: AbsoluteValue R Sabv.eq_zero: β {R : Type ?u.18395} {S : Type ?u.18394} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, βabv x = 0 β x = 0eq_zero.not: β {a b : Prop}, (a β b) β (Β¬a β Β¬b)not
#align absolute_value.ne_zero_iff AbsoluteValue.ne_zero_iff: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
βabv x β  0 β x β  0AbsoluteValue.ne_zero_iff

protected theorem pos: β {x : R}, x β  0 β 0 < βabv xpos {x: Rx : R: Type ?u.18448R} (hx: x β  0hx : x: Rx β  0: ?m.184860) : 0: ?m.186620 < abv: AbsoluteValue R Sabv x: Rx :=
lt_of_le_of_ne: β {Ξ± : Type ?u.19503} [inst : PartialOrder Ξ±] {a b : Ξ±}, a β€ b β a β  b β a < blt_of_le_of_ne (abv: AbsoluteValue R Sabv.nonneg: β {R : Type ?u.19676} {S : Type ?u.19675} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
(x : R), 0 β€ βabv xnonneg x: Rx) (Ne.symm: β {Ξ± : Sort ?u.19704} {a b : Ξ±}, a β  b β b β  aNe.symm <| mt: β {a b : Prop}, (a β b) β Β¬b β Β¬amt abv: AbsoluteValue R Sabv.eq_zero: β {R : Type ?u.19718} {S : Type ?u.19717} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, βabv x = 0 β x = 0eq_zero.mp: β {a b : Prop}, (a β b) β a β bmp hx: x β  0hx)
#align absolute_value.pos AbsoluteValue.pos: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
x β  0 β 0 < βabv xAbsoluteValue.pos

@[simp]
protected theorem pos_iff: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
0 < βabv x β x β  0pos_iff {x: Rx : R: Type ?u.19755R} : 0: ?m.197920 < abv: AbsoluteValue R Sabv x: Rx β x: Rx β  0: ?m.206330 :=
β¨fun hβ: ?m.20814hβ => mt: β {a b : Prop}, (a β b) β Β¬b β Β¬amt abv: AbsoluteValue R Sabv.eq_zero: β {R : Type ?u.20821} {S : Type ?u.20820} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, βabv x = 0 β x = 0eq_zero.mpr: β {a b : Prop}, (a β b) β b β ampr hβ: ?m.20814hβ.ne': β {Ξ± : Type ?u.20854} [inst : Preorder Ξ±] {x y : Ξ±}, x < y β y β  xne', abv: AbsoluteValue R Sabv.pos: β {R : Type ?u.21009} {S : Type ?u.21010} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, x β  0 β 0 < βabv xposβ©
#align absolute_value.pos_iff AbsoluteValue.pos_iff: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
0 < βabv x β x β  0AbsoluteValue.pos_iff

protected theorem ne_zero: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
x β  0 β βabv x β  0ne_zero {x: Rx : R: Type ?u.21080R} (hx: x β  0hx : x: Rx β  0: ?m.211180) : abv: AbsoluteValue R Sabv x: Rx β  0: ?m.217200 :=
(abv: AbsoluteValue R Sabv.pos: β {R : Type ?u.21989} {S : Type ?u.21990} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, x β  0 β 0 < βabv xpos hx: x β  0hx).ne': β {Ξ± : Type ?u.22026} [inst : Preorder Ξ±] {x y : Ξ±}, x < y β y β  xne'
#align absolute_value.ne_zero AbsoluteValue.ne_zero: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
x β  0 β βabv x β  0AbsoluteValue.ne_zero

theorem map_one_of_isLeftRegular: IsLeftRegular (βabv 1) β βabv 1 = 1map_one_of_isLeftRegular (h: IsLeftRegular (βabv 1)h : IsLeftRegular: {R : Type ?u.22224} β [inst : Mul R] β R β PropIsLeftRegular (abv: AbsoluteValue R Sabv 1: ?m.226771)) : abv: AbsoluteValue R Sabv 1: ?m.233431 = 1: ?m.233461 :=
h: IsLeftRegular (βabv 1)h <| byGoals accomplished! π R: Type u_2S: Type u_1instβΒΉ: Semiring Rinstβ: OrderedSemiring Sabv: AbsoluteValue R Sh: IsLeftRegular (βabv 1)(fun x => βabv 1 * x) (βabv 1) = (fun x => βabv 1 * x) 1simp [β map_mul: β {M : Type ?u.23484} {N : Type ?u.23485} {F : Type ?u.23483} [inst : Mul M] [inst_1 : Mul N]
[inst_2 : MulHomClass F M N] (f : F) (x y : M), βf (x * y) = βf x * βf ymap_mul]Goals accomplished! π
#align absolute_value.map_one_of_is_regular AbsoluteValue.map_one_of_isLeftRegular: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
IsLeftRegular (βabv 1) β βabv 1 = 1AbsoluteValue.map_one_of_isLeftRegular

-- Porting note: Removed since `map_zero` proves the theorem
--@[simp]
--protected theorem map_zero : abv 0 = 0 := map_zero _
--abv.eq_zero.2 rfl
#align absolute_value.map_zero map_zero: β {M : Type u_2} {N : Type u_3} {F : Type u_1} [inst : Zero M] [inst_1 : Zero N] [inst_2 : ZeroHomClass F M N] (f : F),
βf 0 = 0map_zero

end Semiring

section Ring

variable {R: Type ?u.27031R S: Type ?u.27236S : Type _: Type (?u.27236+1)Type _} [Ring: Type ?u.27037 β Type ?u.27037Ring R: Type ?u.27233R] [OrderedSemiring: Type ?u.27242 β Type ?u.27242OrderedSemiring S: Type ?u.27236S] (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.27044) β
(S : Type ?u.27043) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.27044?u.27043)AbsoluteValue R: Type ?u.27233R S: Type ?u.38789S)

protected theorem sub_le: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (a b c : R),
βabv (a - c) β€ βabv (a - b) + βabv (b - c)sub_le (a: Ra b: Rb c: Rc : R: Type ?u.27233R) : abv: AbsoluteValue R Sabv (a: Ra - c: Rc) β€ abv: AbsoluteValue R Sabv (a: Ra - b: Rb) + abv: AbsoluteValue R Sabv (b: Rb - c: Rc) := byGoals accomplished! π
R: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: OrderedSemiring Sabv: AbsoluteValue R Sa, b, c: Rβabv (a - c) β€ βabv (a - b) + βabv (b - c)simpa [sub_eq_add_neg: β {G : Type ?u.29361} [inst : SubNegMonoid G] (a b : G), a - b = a + -bsub_eq_add_neg, add_assoc: β {G : Type ?u.29377} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)add_assoc] using abv: AbsoluteValue R Sabv.add_le: β {R : Type ?u.34005} {S : Type ?u.34004} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
(x y : R), βabv (x + y) β€ βabv x + βabv yadd_le (a: Ra - b: Rb) (b: Rb - c: Rc)Goals accomplished! π
#align absolute_value.sub_le AbsoluteValue.sub_le: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (a b c : R),
βabv (a - c) β€ βabv (a - b) + βabv (b - c)AbsoluteValue.sub_le

@[simp (high)]
theorem map_sub_eq_zero_iff: β (a b : R), βabv (a - b) = 0 β a = bmap_sub_eq_zero_iff (a: Ra b: Rb : R: Type ?u.38786R) : abv: AbsoluteValue R Sabv (a: Ra - b: Rb) = 0: ?m.394800 β a: Ra = b: Rb :=
abv: AbsoluteValue R Sabv.eq_zero: β {R : Type ?u.39765} {S : Type ?u.39764} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, βabv x = 0 β x = 0eq_zero.trans: β {a b c : Prop}, (a β b) β (b β c) β (a β c)trans sub_eq_zero: β {G : Type ?u.39980} [inst : AddGroup G] {a b : G}, a - b = 0 β a = bsub_eq_zero
#align absolute_value.map_sub_eq_zero_iff AbsoluteValue.map_sub_eq_zero_iff: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (a b : R),
βabv (a - b) = 0 β a = bAbsoluteValue.map_sub_eq_zero_iff

end Ring

end OrderedSemiring

section OrderedRing

section Semiring

section IsDomain

-- all of these are true for `NoZeroDivisors S`; but it doesn't work smoothly with the
-- `IsDomain`/`CancelMonoidWithZero` API
variable {R: Type ?u.40085R S: Type ?u.40211S : Type _: Type (?u.40419+1)Type _} [Semiring: Type ?u.44594 β Type ?u.44594Semiring R: Type ?u.40085R] [OrderedRing: Type ?u.48083 β Type ?u.48083OrderedRing S: Type ?u.40088S] (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.40432) β
(S : Type ?u.40431) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.40432?u.40431)AbsoluteValue R: Type ?u.40208R S: Type ?u.40088S)

variable [IsDomain: (Ξ± : Type ?u.44711) β [inst : Semiring Ξ±] β PropIsDomain S: Type ?u.40422S] [Nontrivial: Type ?u.42516 β PropNontrivial R: Type ?u.42308R]

@[simp (high)]
protected theorem map_one: βabv 1 = 1map_one : abv: AbsoluteValue R Sabv 1: ?m.410581 = 1: ?m.410951 :=
abv: AbsoluteValue R Sabv.map_one_of_isLeftRegular: β {R : Type ?u.41280} {S : Type ?u.41279} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
IsLeftRegular (βabv 1) β βabv 1 = 1map_one_of_isLeftRegular (isRegular_of_ne_zero: β {R : Type ?u.41403} [inst : CancelMonoidWithZero R] {a : R}, a β  0 β IsRegular aisRegular_of_ne_zero <| abv: AbsoluteValue R Sabv.ne_zero: β {R : Type ?u.41407} {S : Type ?u.41408} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, x β  0 β βabv x β  0ne_zero one_ne_zero: β {Ξ± : Type ?u.41581} [inst : Zero Ξ±] [inst_1 : One Ξ±] [inst_2 : NeZero 1], 1 β  0one_ne_zero).left: β {R : Type ?u.42189} [inst : Mul R] {c : R}, IsRegular c β IsLeftRegular cleft
#align absolute_value.map_one AbsoluteValue.map_one: β {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
[inst_2 : IsDomain S] [inst_3 : Nontrivial R], βabv 1 = 1AbsoluteValue.map_one

instance: {R : Type u_1} β
{S : Type u_2} β
[inst : Semiring R] β
[inst_1 : OrderedRing S] β
[inst_2 : IsDomain S] β [inst_3 : Nontrivial R] β MonoidWithZeroHomClass (AbsoluteValue R S) R Sinstance : MonoidWithZeroHomClass: Type ?u.42521 β
(M : outParam (Type ?u.42520)) β
(N : outParam (Type ?u.42519)) β
[inst : MulZeroOneClass M] β [inst : MulZeroOneClass N] β Type (max(max?u.42521?u.42520)?u.42519)MonoidWithZeroHomClass (AbsoluteValue: (R : Type ?u.42523) β
(S : Type ?u.42522) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.42523?u.42522)AbsoluteValue R: Type ?u.42308R S: Type ?u.42311S) R: Type ?u.42308R S: Type ?u.42311S :=
{ AbsoluteValue.mulHomClass: {R : Type ?u.42750} β
{S : Type ?u.42749} β [inst : Semiring R] β [inst_1 : OrderedSemiring S] β MulHomClass (AbsoluteValue R S) R SAbsoluteValue.mulHomClass with map_zero := fun f: ?m.43396f => map_zero: β {M : Type ?u.43399} {N : Type ?u.43400} {F : Type ?u.43398} [inst : Zero M] [inst_1 : Zero N]
[inst_2 : ZeroHomClass F M N] (f : F), βf 0 = 0map_zero f: ?m.43396f, map_one := fun f: ?m.43339f => f: ?m.43339f.map_one: β {R : Type ?u.43342} {S : Type ?u.43341} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
[inst_2 : IsDomain S] [inst_3 : Nontrivial R], βabv 1 = 1map_one }

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*`, `0` and `1`. -/
def toMonoidWithZeroHom: R β*β StoMonoidWithZeroHom : R: Type ?u.44008R β*β S: Type ?u.44011S :=
abv: AbsoluteValue R Sabv
#align absolute_value.to_monoid_with_zero_hom AbsoluteValue.toMonoidWithZeroHom: {R : Type u_1} β
{S : Type u_2} β
[inst : Semiring R] β
[inst_1 : OrderedRing S] β AbsoluteValue R S β [inst_2 : IsDomain S] β [inst_3 : Nontrivial R] β R β*β SAbsoluteValue.toMonoidWithZeroHom

@[simp]
theorem coe_toMonoidWithZeroHom: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
[inst_2 : IsDomain S] [inst_3 : Nontrivial R], β(toMonoidWithZeroHom abv) = βabvcoe_toMonoidWithZeroHom : βabv: AbsoluteValue R Sabv.toMonoidWithZeroHom: {R : Type ?u.44801} β
{S : Type ?u.44800} β
[inst : Semiring R] β
[inst_1 : OrderedRing S] β AbsoluteValue R S β [inst_2 : IsDomain S] β [inst_3 : Nontrivial R] β R β*β StoMonoidWithZeroHom = abv: AbsoluteValue R Sabv :=
rfl: β {Ξ± : Sort ?u.47283} {a : Ξ±}, a = arfl
#align absolute_value.coe_to_monoid_with_zero_hom AbsoluteValue.coe_toMonoidWithZeroHom: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
[inst_2 : IsDomain S] [inst_3 : Nontrivial R], β(toMonoidWithZeroHom abv) = βabvAbsoluteValue.coe_toMonoidWithZeroHom

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*` and `1`. -/
def toMonoidHom: R β* StoMonoidHom : R: Type ?u.47334R β* S: Type ?u.47337S :=
abv: AbsoluteValue R Sabv
#align absolute_value.to_monoid_hom AbsoluteValue.toMonoidHom: {R : Type u_1} β
{S : Type u_2} β
[inst : Semiring R] β
[inst_1 : OrderedRing S] β AbsoluteValue R S β [inst_2 : IsDomain S] β [inst_3 : Nontrivial R] β R β* SAbsoluteValue.toMonoidHom

@[simp]
theorem coe_toMonoidHom: β(toMonoidHom abv) = βabvcoe_toMonoidHom : βabv: AbsoluteValue R Sabv.toMonoidHom: {R : Type ?u.48287} β
{S : Type ?u.48286} β
[inst : Semiring R] β
[inst_1 : OrderedRing S] β AbsoluteValue R S β [inst_2 : IsDomain S] β [inst_3 : Nontrivial R] β R β* StoMonoidHom = abv: AbsoluteValue R Sabv :=
rfl: β {Ξ± : Sort ?u.50674} {a : Ξ±}, a = arfl
#align absolute_value.coe_to_monoid_hom AbsoluteValue.coe_toMonoidHom: β {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
[inst_2 : IsDomain S] [inst_3 : Nontrivial R], β(toMonoidHom abv) = βabvAbsoluteValue.coe_toMonoidHom

-- Porting note: Removed since `map_zero` proves the theorem
--@[simp]
--protected theorem map_pow (a : R) (n : β) : abv (a ^ n) = abv a ^ n := map_pow _ _ _
--abv.toMonoidHom.map_pow a n
#align absolute_value.map_pow map_pow: β {G : Type u_1} {H : Type u_2} {F : Type u_3} [inst : Monoid G] [inst_1 : Monoid H] [inst_2 : MonoidHomClass F G H]
(f : F) (a : G) (n : β), βf (a ^ n) = βf a ^ nmap_pow

end IsDomain

end Semiring

section Ring

variable {R: Type ?u.51017R S: Type ?u.51020S : Type _: Type (?u.51020+1)Type _} [Ring: Type ?u.50731 β Type ?u.50731Ring R: Type ?u.50725R] [OrderedRing: Type ?u.50734 β Type ?u.50734OrderedRing S: Type ?u.51020S] (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.50738) β
(S : Type ?u.50737) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.50738?u.50737)AbsoluteValue R: Type ?u.50725R S: Type ?u.50728S)

protected theorem le_sub: β (a b : R), βabv a - βabv b β€ βabv (a - b)le_sub (a: Ra b: Rb : R: Type ?u.51017R) : abv: AbsoluteValue R Sabv a: Ra - abv: AbsoluteValue R Sabv b: Rb β€ abv: AbsoluteValue R Sabv (a: Ra - b: Rb) :=
sub_le_iff_le_add: β {Ξ± : Type ?u.52859} [inst : AddGroup Ξ±] [inst_1 : LE Ξ±]
[inst_2 : CovariantClass Ξ± Ξ± (Function.swap fun x x_1 => x + x_1) fun x x_1 => x β€ x_1] {a b c : Ξ±},
a - c β€ b β a β€ b + csub_le_iff_le_add.2: β {a b : Prop}, (a β b) β b β a2 <| byGoals accomplished! π R: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: OrderedRing Sabv: AbsoluteValue R Sa, b: Rβabv a β€ βabv (a - b) + βabv bsimpa using abv: AbsoluteValue R Sabv.add_le: β {R : Type ?u.54789} {S : Type ?u.54788} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
(x y : R), βabv (x + y) β€ βabv x + βabv yadd_le (a: Ra - b: Rb) b: RbGoals accomplished! π
#align absolute_value.le_sub AbsoluteValue.le_sub: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
βabv a - βabv b β€ βabv (a - b)AbsoluteValue.le_sub

end Ring

end OrderedRing

section OrderedCommRing

variable {R: Type ?u.57154R S: Type ?u.56663S : Type _: Type (?u.57157+1)Type _} [Ring: Type ?u.57160 β Type ?u.57160Ring R: Type ?u.56410R] [OrderedCommRing: Type ?u.57163 β Type ?u.57163OrderedCommRing S: Type ?u.56413S] (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.56423) β
(S : Type ?u.56422) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.56423?u.56422)AbsoluteValue R: Type ?u.56410R S: Type ?u.56413S)

variable [NoZeroDivisors: (Mβ : Type ?u.57404) β [inst : Mul Mβ] β [inst : Zero Mβ] β PropNoZeroDivisors S: Type ?u.56663S]

@[simp]
protected theorem map_neg: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a : R), βabv (-a) = βabv amap_neg (a: Ra : R: Type ?u.57154R) : abv: AbsoluteValue R Sabv (-a: Ra) = abv: AbsoluteValue R Sabv a: Ra := byGoals accomplished! π
R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rβabv (-a) = βabv aby_cases ha: ?m.58880ha : a: Ra = 0: ?m.585010R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: a = 0posβabv (-a) = βabv aR: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0negβabv (-a) = βabv a;R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: a = 0posβabv (-a) = βabv aR: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0negβabv (-a) = βabv a R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rβabv (-a) = βabv aΒ·R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: a = 0posβabv (-a) = βabv a R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: a = 0posβabv (-a) = βabv aR: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0negβabv (-a) = βabv asimp [ha: ?m.58873ha]Goals accomplished! π
R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rβabv (-a) = βabv arefine'
(mul_self_eq_mul_self_iff: β {R : Type ?u.59891} [inst : CommRing R] [inst_1 : NoZeroDivisors R] {a b : R}, a * a = b * b β a = b β¨ a = -bmul_self_eq_mul_self_iff.mp: β {a b : Prop}, (a β b) β a β bmp (R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0negβabv (-a) = βabv abyGoals accomplished! π R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0βabv (-a) * βabv (-a) = βabv a * βabv arw [R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0βabv (-a) * βabv (-a) = βabv a * βabv aβ map_mul: β {M : Type ?u.59966} {N : Type ?u.59967} {F : Type ?u.59965} [inst : Mul M] [inst_1 : Mul N]
[inst_2 : MulHomClass F M N] (f : F) (x y : M), βf (x * y) = βf x * βf ymap_mul abv: AbsoluteValue R Sabv,R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0βabv (-a * -a) = βabv a * βabv a R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0βabv (-a) * βabv (-a) = βabv a * βabv aneg_mul_neg: β {Ξ± : Type ?u.60176} [inst : Mul Ξ±] [inst_1 : HasDistribNeg Ξ±] (a b : Ξ±), -a * -b = a * bneg_mul_neg,R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0βabv (a * a) = βabv a * βabv a R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0βabv (-a) * βabv (-a) = βabv a * βabv amap_mul: β {M : Type ?u.60295} {N : Type ?u.60296} {F : Type ?u.60294} [inst : Mul M] [inst_1 : Mul N]
[inst_2 : MulHomClass F M N] (f : F) (x y : M), βf (x * y) = βf x * βf ymap_mul abv: AbsoluteValue R SabvR: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0βabv a * βabv a = βabv a * βabv a]Goals accomplished! π)).resolve_right: β {a b : Prop}, a β¨ b β Β¬b β aresolve_right _: Β¬?m.59928_R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rha: Β¬a = 0negΒ¬βabv (-a) = -βabv a
R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa: Rβabv (-a) = βabv aexact ((neg_lt_zero: β {Ξ± : Type ?u.60404} [inst : AddGroup Ξ±] [inst_1 : LT Ξ±]
[inst_2 : CovariantClass Ξ± Ξ± (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : Ξ±}, -a < 0 β 0 < aneg_lt_zero.mpr: β {a b : Prop}, (a β b) β b β ampr (abv: AbsoluteValue R Sabv.pos: β {R : Type ?u.60453} {S : Type ?u.60454} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, x β  0 β 0 < βabv xpos ha: ?m.58880ha)).trans: β {Ξ± : Type ?u.60736} [inst : Preorder Ξ±] {a b c : Ξ±}, a < b β b < c β a < ctrans (abv: AbsoluteValue R Sabv.pos: β {R : Type ?u.60834} {S : Type ?u.60835} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, x β  0 β 0 < βabv xpos (neg_ne_zero: β {Ξ± : Type ?u.60860} [inst : SubtractionMonoid Ξ±] {a : Ξ±}, -a β  0 β a β  0neg_ne_zero.mpr: β {a b : Prop}, (a β b) β b β ampr ha: ?m.58880ha))).ne': β {Ξ± : Type ?u.60952} [inst : Preorder Ξ±] {x y : Ξ±}, x < y β y β  xne'Goals accomplished! π
#align absolute_value.map_neg AbsoluteValue.map_neg: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a : R), βabv (-a) = βabv aAbsoluteValue.map_neg

protected theorem map_sub: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a b : R), βabv (a - b) = βabv (b - a)map_sub (a: Ra b: Rb : R: Type ?u.61436R) : abv: AbsoluteValue R Sabv (a: Ra - b: Rb) = abv: AbsoluteValue R Sabv (b: Rb - a: Ra) := byGoals accomplished! π R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa, b: Rβabv (a - b) = βabv (b - a)rw [R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa, b: Rβabv (a - b) = βabv (b - a)β neg_sub: β {Ξ± : Type ?u.62855} [inst : SubtractionMonoid Ξ±] (a b : Ξ±), -(a - b) = b - aneg_sub,R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa, b: Rβabv (-(b - a)) = βabv (b - a) R: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa, b: Rβabv (a - b) = βabv (b - a)abv: AbsoluteValue R Sabv.map_neg: β {R : Type ?u.62986} {S : Type ?u.62985} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a : R), βabv (-a) = βabv amap_negR: Type u_2S: Type u_1instβΒ²: Ring RinstβΒΉ: OrderedCommRing Sabv: AbsoluteValue R Sinstβ: NoZeroDivisors Sa, b: Rβabv (b - a) = βabv (b - a)]Goals accomplished! π
#align absolute_value.map_sub AbsoluteValue.map_sub: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a b : R), βabv (a - b) = βabv (b - a)AbsoluteValue.map_sub

end OrderedCommRing

section LinearOrderedRing

variable {R: Type ?u.63068R S: Type ?u.63071S : Type _: Type (?u.64298+1)Type _} [Semiring: Type ?u.63177 β Type ?u.63177Semiring R: Type ?u.63068R] [LinearOrderedRing: Type ?u.63180 β Type ?u.63180LinearOrderedRing S: Type ?u.63174S] (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.63184) β
(S : Type ?u.63183) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.63184?u.63183)AbsoluteValue R: Type ?u.63068R S: Type ?u.63174S)

/-- `AbsoluteValue.abs` is `abs` as a bundled `AbsoluteValue`. -/
@[simps: β {S : Type u_1} [inst : LinearOrderedRing S] (a : S), βAbsoluteValue.abs a = abs asimps]
protected def abs: AbsoluteValue S Sabs : AbsoluteValue: (R : Type ?u.63275) β
(S : Type ?u.63274) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.63275?u.63274)AbsoluteValue S: Type ?u.63174S S: Type ?u.63174S where
toFun := abs: {Ξ± : Type ?u.63450} β [self : Abs Ξ±] β Ξ± β Ξ±abs
nonneg' := abs_nonneg: β {Ξ± : Type ?u.63647} [inst : AddGroup Ξ±] [inst_1 : LinearOrder Ξ±]
[inst_2 : CovariantClass Ξ± Ξ± (fun x x_1 => x + x_1) fun x x_1 => x β€ x_1] (a : Ξ±), 0 β€ abs aabs_nonneg
eq_zero' _: ?m.63849_ := abs_eq_zero: β {Ξ± : Type ?u.63851} [inst : AddGroup Ξ±] [inst_1 : LinearOrder Ξ±]
[inst_2 : CovariantClass Ξ± Ξ± (fun x x_1 => x + x_1) fun x x_1 => x β€ x_1] {a : Ξ±}, abs a = 0 β a = 0abs_eq_zero
add_le' := abs_add: β {Ξ± : Type ?u.63921} [inst : LinearOrderedAddCommGroup Ξ±] (a b : Ξ±), abs (a + b) β€ abs a + abs babs_add
map_mul' := abs_mul: β {Ξ± : Type ?u.63603} [inst : LinearOrderedRing Ξ±] (a b : Ξ±), abs (a * b) = abs a * abs babs_mul
#align absolute_value.abs AbsoluteValue.abs: {S : Type u_1} β [inst : LinearOrderedRing S] β AbsoluteValue S SAbsoluteValue.abs
#align absolute_value.abs_apply AbsoluteValue.abs_apply: β {S : Type u_1} [inst : LinearOrderedRing S] (a : S), βAbsoluteValue.abs a = abs aAbsoluteValue.abs_apply
#align absolute_value.abs_to_mul_hom_apply AbsoluteValue.abs_apply: β {S : Type u_1} [inst : LinearOrderedRing S] (a : S), βAbsoluteValue.abs a = abs aAbsoluteValue.abs_apply

instance: {S : Type u_1} β [inst : LinearOrderedRing S] β Inhabited (AbsoluteValue S S)instance : Inhabited: Sort ?u.64398 β Sort (max1?u.64398)Inhabited (AbsoluteValue: (R : Type ?u.64400) β
(S : Type ?u.64399) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.64400?u.64399)AbsoluteValue S: Type ?u.64298S S: Type ?u.64298S) :=
β¨AbsoluteValue.abs: {S : Type ?u.64520} β [inst : LinearOrderedRing S] β AbsoluteValue S SAbsoluteValue.absβ©

end LinearOrderedRing

section LinearOrderedCommRing

variable {R: Type ?u.64581R S: Type ?u.64820S : Type _: Type (?u.64820+1)Type _} [Ring: Type ?u.64823 β Type ?u.64823Ring R: Type ?u.64581R] [LinearOrderedCommRing: Type ?u.64590 β Type ?u.64590LinearOrderedCommRing S: Type ?u.64584S] (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.64594) β
(S : Type ?u.64593) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.64594?u.64593)AbsoluteValue R: Type ?u.64581R S: Type ?u.64584S)

theorem abs_abv_sub_le_abv_sub: β (a b : R), abs (βabv a - βabv b) β€ βabv (a - b)abs_abv_sub_le_abv_sub (a: Ra b: Rb : R: Type ?u.64817R) : abs: {Ξ± : Type ?u.65058} β [self : Abs Ξ±] β Ξ± β Ξ±abs (abv: AbsoluteValue R Sabv a: Ra - abv: AbsoluteValue R Sabv b: Rb) β€ abv: AbsoluteValue R Sabv (a: Ra - b: Rb) :=
abs_sub_le_iff: β {Ξ± : Type ?u.66670} [inst : LinearOrderedAddCommGroup Ξ±] {a b c : Ξ±}, abs (a - b) β€ c β a - b β€ c β§ b - a β€ cabs_sub_le_iff.2: β {a b : Prop}, (a β b) β b β a2 β¨abv: AbsoluteValue R Sabv.le_sub: β {R : Type ?u.66746} {S : Type ?u.66745} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
βabv a - βabv b β€ βabv (a - b)le_sub _: ?m.66754_ _: ?m.66754_, byGoals accomplished! π R: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: LinearOrderedCommRing Sabv: AbsoluteValue R Sa, b: Rβabv b - βabv a β€ βabv (a - b)rw [R: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: LinearOrderedCommRing Sabv: AbsoluteValue R Sa, b: Rβabv b - βabv a β€ βabv (a - b)abv: AbsoluteValue R Sabv.map_sub: β {R : Type ?u.66876} {S : Type ?u.66875} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a b : R), βabv (a - b) = βabv (b - a)map_subR: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: LinearOrderedCommRing Sabv: AbsoluteValue R Sa, b: Rβabv b - βabv a β€ βabv (b - a)]R: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: LinearOrderedCommRing Sabv: AbsoluteValue R Sa, b: Rβabv b - βabv a β€ βabv (b - a);R: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: LinearOrderedCommRing Sabv: AbsoluteValue R Sa, b: Rβabv b - βabv a β€ βabv (b - a) R: Type u_2S: Type u_1instβΒΉ: Ring Rinstβ: LinearOrderedCommRing Sabv: AbsoluteValue R Sa, b: Rβabv b - βabv a β€ βabv (a - b)apply abv: AbsoluteValue R Sabv.le_sub: β {R : Type ?u.67104} {S : Type ?u.67103} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
βabv a - βabv b β€ βabv (a - b)le_subGoals accomplished! πβ©
#align absolute_value.abs_abv_sub_le_abv_sub AbsoluteValue.abs_abv_sub_le_abv_sub: β {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst_1 : LinearOrderedCommRing S] (abv : AbsoluteValue R S) (a b : R),
abs (βabv a - βabv b) β€ βabv (a - b)AbsoluteValue.abs_abv_sub_le_abv_sub

end LinearOrderedCommRing

end AbsoluteValue

-- Porting note: Removed [] in fields, see
-- leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infer.20kinds.20are.20unsupported

/-- A function `f` is an absolute value if it is nonnegative, zero only at 0, additive, and
multiplicative.
See also the type `AbsoluteValue` which represents a bundled version of absolute values.
-/
class IsAbsoluteValue: {S : Type u_1} β [inst : OrderedSemiring S] β {R : Type u_2} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue {S: ?m.67135S} [OrderedSemiring: Type ?u.67138 β Type ?u.67138OrderedSemiring S: ?m.67135S] {R: ?m.67141R} [Semiring: Type ?u.67144 β Type ?u.67144Semiring R: ?m.67141R] (f: R β Sf : R: ?m.67141R β S: ?m.67135S) : Prop: TypeProp where
/-- The absolute value is nonnegative -/
abv_nonneg': β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R β S} [self : IsAbsoluteValue f]
(x : R), 0 β€ f xabv_nonneg' : β x: ?m.67153x, 0: ?m.671580 β€ f: R β Sf x: ?m.67153x
/-- The absolute value is positive definitive -/
abv_eq_zero': β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R β S} [self : IsAbsoluteValue f]
{x : R}, f x = 0 β x = 0abv_eq_zero' : β {x: ?m.67487x}, f: R β Sf x: ?m.67487x = 0: ?m.674920 β x: ?m.67487x = 0: ?m.675100
/-- The absolute value satisfies the triangle inequality -/
abv_add': β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R β S} [self : IsAbsoluteValue f]
(x y : R), f (x + y) β€ f x + f yabv_add' : β x: ?m.67698x y: ?m.67701y, f: R β Sf (x: ?m.67698x + y: ?m.67701y) β€ f: R β Sf x: ?m.67698x + f: R β Sf y: ?m.67701y
/-- The absolute value is multiplicative -/
abv_mul': β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] {f : R β S} [self : IsAbsoluteValue f]
(x y : R), f (x * y) = f x * f yabv_mul' : β x: ?m.68272x y: ?m.68275y, f: R β Sf (x: ?m.68272x * y: ?m.68275y) = f: R β Sf x: ?m.68272x * f: R β Sf y: ?m.68275y
#align is_absolute_value IsAbsoluteValue: {S : Type u_1} β [inst : OrderedSemiring S] β {R : Type u_2} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue

namespace IsAbsoluteValue

section OrderedSemiring

variable {S: Type ?u.71634S : Type _: Type (?u.71054+1)Type _} [OrderedSemiring: Type ?u.72493 β Type ?u.72493OrderedSemiring S: Type ?u.68820S]

variable {R: Type ?u.68890R : Type _: Type (?u.72496+1)Type _} [Semiring: Type ?u.71643 β Type ?u.71643Semiring R: Type ?u.68890R] (abv: R β Sabv : R: Type ?u.68890R β S: Type ?u.72490S) [IsAbsoluteValue: {S : Type ?u.71071} β [inst : OrderedSemiring S] β {R : Type ?u.71070} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv]

lemma abv_nonneg: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x : R), 0 β€ abv xabv_nonneg (x: Rx) : 0: ?m.689470 β€ abv: R β Sabv x: ?m.68942x := abv_nonneg': β {S : Type ?u.69277} [inst : OrderedSemiring S] {R : Type ?u.69276} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] (x : R), 0 β€ f xabv_nonneg' x: Rx
#align is_absolute_value.abv_nonneg IsAbsoluteValue.abv_nonneg: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x : R), 0 β€ abv xIsAbsoluteValue.abv_nonneg

open Lean Meta Mathlib Meta Positivity Qq in
/-- The `positivity` extension which identifies expressions of the form `abv a`. -/
@[positivity (_: Ξ±_ : Ξ±: ?m.71047Ξ±)]
def Mathlib.Meta.Positivity.evalAbv: PositivityExtMathlib.Meta.Positivity.evalAbv : PositivityExt: TypePositivityExt where eval {_: ?m.69415_ _Ξ±: ?m.69418_Ξ±} _zΞ±: ?m.69421_zΞ± _pΞ±: ?m.69424_pΞ± e: ?m.69427e := do
let (.app: Expr β Expr β Expr.app f: Exprf a: Expra) β whnfR: Expr β MetaM ExprwhnfR e: ?m.69427e | throwError "not abv Β·": ?m.69679 ?m.69680throwErrorthrowError "not abv Β·": ?m.69679 ?m.69680 "not abv Β·"
let pa': ?m.69581pa' β mkAppM: Name β Array Expr β MetaM ExprmkAppM ``abv_nonneg: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x : R), 0 β€ abv xabv_nonneg #[f: Exprf, a: Expra]
pure: {f : Type ?u.69584 β Type ?u.69583} β [self : Pure f] β {Ξ± : Type ?u.69584} β Ξ± β f Ξ±pure (.nonnegative: {u : Level} β
{Ξ± : Q(Type u)} β {zΞ± : Q(Zero Β«\$Ξ±Β»)} β {pΞ± : Q(PartialOrder Β«\$Ξ±Β»)} β {e : Q(Β«\$Ξ±Β»)} β Q(0 β€ Β«\$eΒ») β Strictness zΞ± pΞ± e.nonnegative pa': ?m.69581pa')

lemma abv_eq_zero: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] {x : R}, abv x = 0 β x = 0abv_eq_zero {x: Rx} : abv: R β Sabv x: ?m.71112x = 0: ?m.711170 β x: ?m.71112x = 0: ?m.713460 := abv_eq_zero': β {S : Type ?u.71535} [inst : OrderedSemiring S] {R : Type ?u.71534} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] {x : R}, f x = 0 β x = 0abv_eq_zero'
#align is_absolute_value.abv_eq_zero IsAbsoluteValue.abv_eq_zero: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] {x : R}, abv x = 0 β x = 0IsAbsoluteValue.abv_eq_zero

lemma abv_add: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x + y) β€ abv x + abv yabv_add (x: ?m.71692x y: ?m.71695y) : abv: R β Sabv (x: ?m.71692x + y: ?m.71695y) β€ abv: R β Sabv x: ?m.71692x + abv: R β Sabv y: ?m.71695y := abv_add': β {S : Type ?u.72402} [inst : OrderedSemiring S] {R : Type ?u.72401} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] (x y : R), f (x + y) β€ f x + f yabv_add' x: Rx y: Ry
#align is_absolute_value.abv_add IsAbsoluteValue.abv_add: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x + y) β€ abv x + abv yIsAbsoluteValue.abv_add

lemma abv_mul: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv yabv_mul (x: ?m.72548x y: ?m.72551y) : abv: R β Sabv (x: ?m.72548x * y: ?m.72551y) = abv: R β Sabv x: ?m.72548x * abv: R β Sabv y: ?m.72551y := abv_mul': β {S : Type ?u.73180} [inst : OrderedSemiring S] {R : Type ?u.73179} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] (x y : R), f (x * y) = f x * f yabv_mul' x: Rx y: Ry
#align is_absolute_value.abv_mul IsAbsoluteValue.abv_mul: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv yIsAbsoluteValue.abv_mul

/-- A bundled absolute value is an absolute value. -/
instance _root_.AbsoluteValue.isAbsoluteValue: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : AbsoluteValue R S),
IsAbsoluteValue βabv_root_.AbsoluteValue.isAbsoluteValue (abv: AbsoluteValue R Sabv : AbsoluteValue: (R : Type ?u.73318) β
(S : Type ?u.73317) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.73318?u.73317)AbsoluteValue R: Type ?u.73265R S: Type ?u.73259S) :
IsAbsoluteValue: {S : Type ?u.73339} β [inst : OrderedSemiring S] β {R : Type ?u.73338} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: AbsoluteValue R Sabv where
abv_nonneg' := abv: AbsoluteValue R Sabv.nonneg: β {R : Type ?u.73799} {S : Type ?u.73798} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
(x : R), 0 β€ βabv xnonneg
abv_eq_zero' := abv: AbsoluteValue R Sabv.eq_zero: β {R : Type ?u.73819} {S : Type ?u.73818} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, βabv x = 0 β x = 0eq_zero
abv_add' := abv: AbsoluteValue R Sabv.add_le: β {R : Type ?u.73850} {S : Type ?u.73849} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
(x y : R), βabv (x + y) β€ βabv x + βabv yadd_le
abv_mul' := abv: AbsoluteValue R Sabv.map_mul: β {M : Type ?u.73880} {N : Type ?u.73881} [inst : Mul M] [inst_1 : Mul N] (f : M ββ* N) (a b : M),
βf (a * b) = βf a * βf bmap_mul
#align absolute_value.is_absolute_value AbsoluteValue.isAbsoluteValue: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : AbsoluteValue R S),
IsAbsoluteValue βabvAbsoluteValue.isAbsoluteValue

/-- Convert an unbundled `IsAbsoluteValue` to a bundled `AbsoluteValue`. -/
@[simps: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (a : R), β(toAbsoluteValue abv) a = abv asimps]
def toAbsoluteValue: {S : Type u_1} β
[inst : OrderedSemiring S] β
{R : Type u_2} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue : AbsoluteValue: (R : Type ?u.74334) β
(S : Type ?u.74333) β [inst : Semiring R] β [inst : OrderedSemiring S] β Type (max?u.74334?u.74333)AbsoluteValue R: Type ?u.74281R S: Type ?u.74275S where
toFun := abv: R β Sabv
add_le' := abv_add': β {S : Type ?u.74913} [inst : OrderedSemiring S] {R : Type ?u.74912} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] (x y : R), f (x + y) β€ f x + f yabv_add'
eq_zero' _: ?m.74856_ := abv_eq_zero': β {S : Type ?u.74859} [inst : OrderedSemiring S] {R : Type ?u.74858} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] {x : R}, f x = 0 β x = 0abv_eq_zero'
nonneg' := abv_nonneg': β {S : Type ?u.74788} [inst : OrderedSemiring S] {R : Type ?u.74787} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] (x : R), 0 β€ f xabv_nonneg'
map_mul' := abv_mul': β {S : Type ?u.74696} [inst : OrderedSemiring S] {R : Type ?u.74695} [inst_1 : Semiring R] {f : R β S}
[self : IsAbsoluteValue f] (x y : R), f (x * y) = f x * f yabv_mul'
#align is_absolute_value.to_absolute_value IsAbsoluteValue.toAbsoluteValue: {S : Type u_1} β
[inst : OrderedSemiring S] β
{R : Type u_2} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R SIsAbsoluteValue.toAbsoluteValue
#align is_absolute_value.to_absolute_value_apply IsAbsoluteValue.toAbsoluteValue_apply: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (a : R), β(toAbsoluteValue abv) a = abv aIsAbsoluteValue.toAbsoluteValue_apply
#align is_absolute_value.to_absolute_value_to_mul_hom_apply IsAbsoluteValue.toAbsoluteValue_apply: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (a : R), β(toAbsoluteValue abv) a = abv aIsAbsoluteValue.toAbsoluteValue_apply

theorem abv_zero: abv 0 = 0abv_zero : abv: R β Sabv 0: ?m.751720 = 0: ?m.753450 :=
map_zero: β {M : Type ?u.75574} {N : Type ?u.75575} {F : Type ?u.75573} [inst : Zero M] [inst_1 : Zero N]
[inst_2 : ZeroHomClass F M N] (f : F), βf 0 = 0map_zero (toAbsoluteValue: {S : Type ?u.75583} β
[inst : OrderedSemiring S] β
{R : Type ?u.75582} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv)
#align is_absolute_value.abv_zero IsAbsoluteValue.abv_zero: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv], abv 0 = 0IsAbsoluteValue.abv_zero

theorem abv_pos: β {a : R}, 0 < abv a β a β  0abv_pos {a: Ra : R: Type ?u.76125R} : 0: ?m.761810 < abv: R β Sabv a: Ra β a: Ra β  0: ?m.765100 :=
(toAbsoluteValue: {S : Type ?u.76685} β
[inst : OrderedSemiring S] β
{R : Type ?u.76684} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).pos_iff: β {R : Type ?u.76723} {S : Type ?u.76722} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, 0 < βabv x β x β  0pos_iff
#align is_absolute_value.abv_pos IsAbsoluteValue.abv_pos: β {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] {a : R}, 0 < abv a β a β  0IsAbsoluteValue.abv_pos

end OrderedSemiring

section LinearOrderedRing

variable {S: Type ?u.76787S : Type _: Type (?u.76787+1)Type _} [LinearOrderedRing: Type ?u.76784 β Type ?u.76784LinearOrderedRing S: Type ?u.76781S]

instance abs_isAbsoluteValue: β {S : Type u_1} [inst : LinearOrderedRing S], IsAbsoluteValue absabs_isAbsoluteValue : IsAbsoluteValue: {S : Type ?u.76794} β [inst : OrderedSemiring S] β {R : Type ?u.76793} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue (abs: {Ξ± : Type ?u.76818} β [self : Abs Ξ±] β Ξ± β Ξ±abs : S: Type ?u.76787S β S: Type ?u.76787S) :=
AbsoluteValue.abs: {S : Type ?u.77088} β [inst : LinearOrderedRing S] β AbsoluteValue S SAbsoluteValue.abs.isAbsoluteValue: β {S : Type ?u.77095} [inst : OrderedSemiring S] {R : Type ?u.77094} [inst_1 : Semiring R] (abv : AbsoluteValue R S),
IsAbsoluteValue βabvisAbsoluteValue
#align is_absolute_value.abs_is_absolute_value IsAbsoluteValue.abs_isAbsoluteValue: β {S : Type u_1} [inst : LinearOrderedRing S], IsAbsoluteValue absIsAbsoluteValue.abs_isAbsoluteValue

end LinearOrderedRing

section OrderedRing

variable {S: Type ?u.77187S : Type _: Type (?u.77335+1)Type _} [OrderedRing: Type ?u.77184 β Type ?u.77184OrderedRing S: Type ?u.77181S]

section Semiring

variable {R: Type ?u.77193R : Type _: Type (?u.77341+1)Type _} [Semiring: Type ?u.78193 β Type ?u.78193Semiring R: Type ?u.77193R] (abv: R β Sabv : R: Type ?u.77574R β S: Type ?u.78792S) [IsAbsoluteValue: {S : Type ?u.77585} β [inst : OrderedSemiring S] β {R : Type ?u.77584} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv]

variable [IsDomain: (Ξ± : Type ?u.78332) β [inst : Semiring Ξ±] β PropIsDomain S: Type ?u.77335S]

theorem abv_one: β [inst : Nontrivial R], abv 1 = 1abv_one [Nontrivial: Type ?u.77801 β PropNontrivial R: Type ?u.77574R] : abv: R β Sabv 1: ?m.778061 = 1: ?m.778451 :=
(toAbsoluteValue: {S : Type ?u.77998} β
[inst : OrderedSemiring S] β
{R : Type ?u.77997} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).map_one: β {R : Type ?u.78126} {S : Type ?u.78125} [inst : Semiring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S)
[inst_2 : IsDomain S] [inst_3 : Nontrivial R], βabv 1 = 1map_one
#align is_absolute_value.abv_one IsAbsoluteValue.abv_one: β {S : Type u_2} [inst : OrderedRing S] {R : Type u_1} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] [inst_3 : IsDomain S] [inst_4 : Nontrivial R], abv 1 = 1IsAbsoluteValue.abv_one

/-- `abv` as a `MonoidWithZeroHom`. -/
def abvHom: [inst : Nontrivial R] β R β*β SabvHom [Nontrivial: Type ?u.78417 β PropNontrivial R: Type ?u.78190R] : R: Type ?u.78190R β*β S: Type ?u.78184S :=
(toAbsoluteValue: {S : Type ?u.78569} β
[inst : OrderedSemiring S] β
{R : Type ?u.78568} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).toMonoidWithZeroHom: {R : Type ?u.78668} β
{S : Type ?u.78667} β
[inst : Semiring R] β
[inst_1 : OrderedRing S] β AbsoluteValue R S β [inst_2 : IsDomain S] β [inst_3 : Nontrivial R] β R β*β StoMonoidWithZeroHom
#align is_absolute_value.abv_hom IsAbsoluteValue.abvHom: {S : Type u_1} β
[inst : OrderedRing S] β
{R : Type u_2} β
[inst_1 : Semiring R] β
(abv : R β S) β [inst_2 : IsAbsoluteValue abv] β [inst_3 : IsDomain S] β [inst_4 : Nontrivial R] β R β*β SIsAbsoluteValue.abvHom

theorem abv_pow: β [inst : Nontrivial R] (abv : R β S) [inst : IsAbsoluteValue abv] (a : R) (n : β), abv (a ^ n) = abv a ^ nabv_pow [Nontrivial: Type ?u.79025 β PropNontrivial R: Type ?u.78798R] (abv: R β Sabv : R: Type ?u.78798R β S: Type ?u.78792S) [IsAbsoluteValue: {S : Type ?u.79033} β [inst : OrderedSemiring S] β {R : Type ?u.79032} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv] (a: Ra : R: Type ?u.78798R) (n: βn : β: Typeβ) :
abv: R β Sabv (a: Ra ^ n: βn) = abv: R β Sabv a: Ra ^ n: βn :=
map_pow: β {G : Type ?u.79563} {H : Type ?u.79564} {F : Type ?u.79565} [inst : Monoid G] [inst_1 : Monoid H]
[inst_2 : MonoidHomClass F G H] (f : F) (a : G) (n : β), βf (a ^ n) = βf a ^ nmap_pow (toAbsoluteValue: {S : Type ?u.79573} β
[inst : OrderedSemiring S] β
{R : Type ?u.79572} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv) a: Ra n: βn
#align is_absolute_value.abv_pow IsAbsoluteValue.abv_pow: β {S : Type u_2} [inst : OrderedRing S] {R : Type u_1} [inst_1 : Semiring R] [inst_2 : IsDomain S]
[inst_3 : Nontrivial R] (abv : R β S) [inst_4 : IsAbsoluteValue abv] (a : R) (n : β), abv (a ^ n) = abv a ^ nIsAbsoluteValue.abv_pow

end Semiring

section Ring

variable {R: Type ?u.80372R : Type _: Type (?u.80055+1)Type _} [Ring: Type ?u.80058 β Type ?u.80058Ring R: Type ?u.80055R] (abv: R β Sabv : R: Type ?u.80055R β S: Type ?u.80049S) [IsAbsoluteValue: {S : Type ?u.80066} β [inst : OrderedSemiring S] β {R : Type ?u.80065} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv]

theorem abv_sub_le: β {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S) [inst_2 : IsAbsoluteValue abv]
(a b c : R), abv (a - c) β€ abv (a - b) + abv (b - c)abv_sub_le (a: Ra b: Rb c: Rc : R: Type ?u.80372R) : abv: R β Sabv (a: Ra - c: Rc) β€ abv: R β Sabv (a: Ra - b: Rb) + abv: R β Sabv (b: Rb - c: Rc) := byGoals accomplished! π
S: Type u_1instβΒ²: OrderedRing SR: Type u_2instβΒΉ: Ring Rabv: R β Sinstβ: IsAbsoluteValue abva, b, c: Rabv (a - c) β€ abv (a - b) + abv (b - c)simpa [sub_eq_add_neg: β {G : Type ?u.81062} [inst : SubNegMonoid G] (a b : G), a - b = a + -bsub_eq_add_neg, add_assoc: β {G : Type ?u.81078} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)add_assoc] using abv_add: β {S : Type ?u.82152} [inst : OrderedSemiring S] {R : Type ?u.82153} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x + y) β€ abv x + abv yabv_add abv: R β Sabv (a: Ra - b: Rb) (b: Rb - c: Rc)Goals accomplished! π
#align is_absolute_value.abv_sub_le IsAbsoluteValue.abv_sub_le: β {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S) [inst_2 : IsAbsoluteValue abv]
(a b c : R), abv (a - c) β€ abv (a - b) + abv (b - c)IsAbsoluteValue.abv_sub_le

theorem sub_abv_le_abv_sub: β {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S) [inst_2 : IsAbsoluteValue abv]
(a b : R), abv a - abv b β€ abv (a - b)sub_abv_le_abv_sub (a: Ra b: Rb : R: Type ?u.83601R) : abv: R β Sabv a: Ra - abv: R β Sabv b: Rb β€ abv: R β Sabv (a: Ra - b: Rb) :=
(toAbsoluteValue: {S : Type ?u.84188} β
[inst : OrderedSemiring S] β
{R : Type ?u.84187} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).le_sub: β {R : Type ?u.84485} {S : Type ?u.84484} [inst : Ring R] [inst_1 : OrderedRing S] (abv : AbsoluteValue R S) (a b : R),
βabv a - βabv b β€ βabv (a - b)le_sub a: Ra b: Rb
#align is_absolute_value.sub_abv_le_abv_sub IsAbsoluteValue.sub_abv_le_abv_sub: β {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S) [inst_2 : IsAbsoluteValue abv]
(a b : R), abv a - abv b β€ abv (a - b)IsAbsoluteValue.sub_abv_le_abv_sub

end Ring

end OrderedRing

section OrderedCommRing

variable {S: Type ?u.84529S : Type _: Type (?u.84535+1)Type _} [OrderedCommRing: Type ?u.84538 β Type ?u.84538OrderedCommRing S: Type ?u.86188S]

section Ring

variable {R: Type ?u.86194R : Type _: Type (?u.85335+1)Type _} [Ring: Type ?u.84544 β Type ?u.84544Ring R: Type ?u.84541R] (abv: R β Sabv : R: Type ?u.84541R β S: Type ?u.84535S) [IsAbsoluteValue: {S : Type ?u.84552} β [inst : OrderedSemiring S] β {R : Type ?u.84551} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv]

variable [NoZeroDivisors: (Mβ : Type ?u.86463) β [inst : Mul Mβ] β [inst : Zero Mβ] β PropNoZeroDivisors S: Type ?u.84810S]

theorem abv_neg: β {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R), abv (-a) = abv aabv_neg (a: Ra : R: Type ?u.85335R) : abv: R β Sabv (-a: Ra) = abv: R β Sabv a: Ra :=
(toAbsoluteValue: {S : Type ?u.85878} β
[inst : OrderedSemiring S] β
{R : Type ?u.85877} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).map_neg: β {R : Type ?u.86133} {S : Type ?u.86132} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a : R), βabv (-a) = βabv amap_neg a: Ra
#align is_absolute_value.abv_neg IsAbsoluteValue.abv_neg: β {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R), abv (-a) = abv aIsAbsoluteValue.abv_neg

theorem abv_sub: β (a b : R), abv (a - b) = abv (b - a)abv_sub (a: Ra b: Rb : R: Type ?u.86194R) : abv: R β Sabv (a: Ra - b: Rb) = abv: R β Sabv (b: Rb - a: Ra) :=
(toAbsoluteValue: {S : Type ?u.86811} β
[inst : OrderedSemiring S] β
{R : Type ?u.86810} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).map_sub: β {R : Type ?u.87066} {S : Type ?u.87065} [inst : Ring R] [inst_1 : OrderedCommRing S] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a b : R), βabv (a - b) = βabv (b - a)map_sub a: Ra b: Rb
#align is_absolute_value.abv_sub IsAbsoluteValue.abv_sub: β {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a b : R), abv (a - b) = abv (b - a)IsAbsoluteValue.abv_sub

end Ring

end OrderedCommRing

section LinearOrderedCommRing

variable {S: Type ?u.87129S : Type _: Type (?u.87123+1)Type _} [LinearOrderedCommRing: Type ?u.87126 β Type ?u.87126LinearOrderedCommRing S: Type ?u.87123S]

section Ring

variable {R: Type ?u.87396R : Type _: Type (?u.87135+1)Type _} [Ring: Type ?u.87138 β Type ?u.87138Ring R: Type ?u.87135R] (abv: R β Sabv : R: Type ?u.87135R β S: Type ?u.87390S) [IsAbsoluteValue: {S : Type ?u.87146} β [inst : OrderedSemiring S] β {R : Type ?u.87145} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv]

theorem abs_abv_sub_le_abv_sub: β {S : Type u_1} [inst : LinearOrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (a b : R), abs (abv a - abv b) β€ abv (a - b)abs_abv_sub_le_abv_sub (a: Ra b: Rb : R: Type ?u.87396R) : abs: {Ξ± : Type ?u.87656} β [self : Abs Ξ±] β Ξ± β Ξ±abs (abv: R β Sabv a: Ra - abv: R β Sabv b: Rb) β€ abv: R β Sabv (a: Ra - b: Rb) :=
(toAbsoluteValue: {S : Type ?u.87973} β
[inst : OrderedSemiring S] β
{R : Type ?u.87972} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).abs_abv_sub_le_abv_sub: β {R : Type ?u.88214} {S : Type ?u.88213} [inst : Ring R] [inst_1 : LinearOrderedCommRing S] (abv : AbsoluteValue R S)
(a b : R), abs (βabv a - βabv b) β€ βabv (a - b)abs_abv_sub_le_abv_sub a: Ra b: Rb
#align is_absolute_value.abs_abv_sub_le_abv_sub IsAbsoluteValue.abs_abv_sub_le_abv_sub: β {S : Type u_1} [inst : LinearOrderedCommRing S] {R : Type u_2} [inst_1 : Ring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (a b : R), abs (abv a - abv b) β€ abv (a - b)IsAbsoluteValue.abs_abv_sub_le_abv_sub

end Ring

end LinearOrderedCommRing

section LinearOrderedField

variable {S: Type ?u.90880S : Type _: Type (?u.88273+1)Type _} [LinearOrderedSemifield: Type ?u.88276 β Type ?u.88276LinearOrderedSemifield S: Type ?u.88273S]

section Semiring

variable {R: Type ?u.88373R : Type _: Type (?u.88285+1)Type _} [Semiring: Type ?u.88288 β Type ?u.88288Semiring R: Type ?u.88285R] [Nontrivial: Type ?u.88291 β PropNontrivial R: Type ?u.88285R] (abv: R β Sabv : R: Type ?u.88285R β S: Type ?u.88279S) [IsAbsoluteValue: {S : Type ?u.88299} β [inst : OrderedSemiring S] β {R : Type ?u.88298} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv]

theorem abv_one': abv 1 = 1abv_one' : abv: R β Sabv 1: ?m.884571 = 1: ?m.884961 :=
(toAbsoluteValue: {S : Type ?u.88574} β
[inst : OrderedSemiring S] β
{R : Type ?u.88573} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).map_one_of_isLeftRegular: β {R : Type ?u.88639} {S : Type ?u.88638} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S),
IsLeftRegular (βabv 1) β βabv 1 = 1map_one_of_isLeftRegular <|
(isRegular_of_ne_zero: β {R : Type ?u.88657} [inst : CancelMonoidWithZero R] {a : R}, a β  0 β IsRegular aisRegular_of_ne_zero <| (toAbsoluteValue: {S : Type ?u.88662} β
[inst : OrderedSemiring S] β
{R : Type ?u.88661} β [inst_1 : Semiring R] β (abv : R β S) β [inst_2 : IsAbsoluteValue abv] β AbsoluteValue R StoAbsoluteValue abv: R β Sabv).ne_zero: β {R : Type ?u.88671} {S : Type ?u.88672} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
{x : R}, x β  0 β βabv x β  0ne_zero one_ne_zero: β {Ξ± : Type ?u.89176} [inst : Zero Ξ±] [inst_1 : One Ξ±] [inst_2 : NeZero 1], 1 β  0one_ne_zero).left: β {R : Type ?u.89955} [inst : Mul R] {c : R}, IsRegular c β IsLeftRegular cleft
#align is_absolute_value.abv_one' IsAbsoluteValue.abv_one': β {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : Nontrivial R]
(abv : R β S) [inst_3 : IsAbsoluteValue abv], abv 1 = 1IsAbsoluteValue.abv_one'

/-- An absolute value as a monoid with zero homomorphism, assuming the target is a semifield. -/
def abvHom': R β*β SabvHom' : R: Type ?u.90155R β*β S: Type ?u.90149S :=
β¨β¨abv: R β Sabv, abv_zero: β {S : Type ?u.90438} [inst : OrderedSemiring S] {R : Type ?u.90439} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv], abv 0 = 0abv_zero abv: R β Sabvβ©, abv_one': β {S : Type ?u.90706} [inst : LinearOrderedSemifield S] {R : Type ?u.90707} [inst_1 : Semiring R]
[inst_2 : Nontrivial R] (abv : R β S) [inst_3 : IsAbsoluteValue abv], abv 1 = 1abv_one' abv: R β Sabv, abv_mul: β {S : Type ?u.90734} [inst : OrderedSemiring S] {R : Type ?u.90735} [inst_1 : Semiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv yabv_mul abv: R β Sabvβ©
#align is_absolute_value.abv_hom' IsAbsoluteValue.abvHom': {S : Type u_1} β
[inst : LinearOrderedSemifield S] β
{R : Type u_2} β
[inst_1 : Semiring R] β [inst_2 : Nontrivial R] β (abv : R β S) β [inst_3 : IsAbsoluteValue abv] β R β*β SIsAbsoluteValue.abvHom'

end Semiring

section DivisionSemiring

variable {R: Type ?u.91080R : Type _: Type (?u.92071+1)Type _} [DivisionSemiring: Type ?u.90889 β Type ?u.90889DivisionSemiring R: Type ?u.90886R] (abv: R β Sabv : R: Type ?u.90886R β S: Type ?u.90880S) [IsAbsoluteValue: {S : Type ?u.91091} β [inst : OrderedSemiring S] β {R : Type ?u.91090} β [inst : Semiring R] β (R β S) β PropIsAbsoluteValue abv: R β Sabv]

theorem abv_inv: β (a : R), abv aβ»ΒΉ = (abv a)β»ΒΉabv_inv (a: Ra : R: Type ?u.91080R) : abv: R β Sabv a: Raβ»ΒΉ = (abv: R β Sabv a: Ra)β»ΒΉ :=
map_invβ: β {Gβ : Type ?u.91391} {Gβ' : Type ?u.91390} {F : Type ?u.91392} [inst : GroupWithZero Gβ] [inst_1 : GroupWithZero Gβ']
[inst_2 : MonoidWithZeroHomClass F Gβ Gβ'] (f : F) (a : Gβ), βf aβ»ΒΉ = (βf a)β»ΒΉmap_invβ (abvHom': {S : Type ?u.91400} β
[inst : LinearOrderedSemifield S] β
{R : Type ?u.91399} β
[inst_1 : Semiring R] β [inst_2 : Nontrivial R] β (abv : R β S) β [inst_3 : IsAbsoluteValue abv] β R β*β SabvHom' abv: R β Sabv) a: Ra
#align is_absolute_value.abv_inv IsAbsoluteValue.abv_inv: β {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst_1 : DivisionSemiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (a : R), abv aβ»ΒΉ = (abv a)β»ΒΉIsAbsoluteValue.abv_inv

theorem abv_div: β (a b : R), abv (a / b) = abv a / abv babv_div (a: Ra b: Rb : R: Type ?u.92071R) : abv: R β Sabv (a: Ra / b: Rb) = abv: R β Sabv a: Ra / abv: R β Sabv b: Rb :=
map_divβ: β {Gβ : Type ?u.92467} {Gβ' : Type ?u.92466} {F : Type ?u.92468} [inst : GroupWithZero Gβ] [inst_1 : GroupWithZero Gβ']
[inst_2 : MonoidWithZeroHomClass F Gβ Gβ'] (f : F) (a b : Gβ), βf (a / b) = βf a / βf bmap_divβ (abvHom': {S : Type ?u.92476} β
[inst : LinearOrderedSemifield S] β
{R : Type ?u.92475} β
[inst_1 : Semiring R] β [inst_2 : Nontrivial R] β (abv : R β S) β [inst_3 : IsAbsoluteValue abv] β R β*β SabvHom' abv: R β Sabv) a: Ra b: Rb
#align is_absolute_value.abv_div IsAbsoluteValue.abv_div: β {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst_1 : DivisionSemiring R] (abv : R β S)
[inst_2 : IsAbsoluteValue abv] (a b : R), abv (a / b) = abv a / abv bIsAbsoluteValue.abv_div

end DivisionSemiring

end LinearOrderedField

end IsAbsoluteValue
```