Valuation.ne_zero_iff
theorem Valuation.ne_zero_iff :
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
[inst_2 : Nontrivial Γ₀] (v : Valuation K Γ₀) {x : K}, v x ≠ 0 ↔ x ≠ 0
The theorem `Valuation.ne_zero_iff` states that for every division ring `K` and every non-trivial, linearly ordered commutative monoid with zero `Γ₀`, for a valuation `v` from `K` to `Γ₀`, a non-zero value `x` in `K` is associated with a non-zero value in `Γ₀` under the valuation `v`. In other words, `v` of `x` is not equal to zero if and only if `x` is not equal to zero.
More concisely: For every division ring K and non-trivial, linearly ordered commutative monoid with zero Γ₀, a valuation v from K to Γ₀ maps non-zero elements in K to non-zero elements in Γ₀.
|
Valuation.one_lt_val_iff
theorem Valuation.one_lt_val_iff :
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
(v : Valuation K Γ₀) {x : K}, x ≠ 0 → (1 < v x ↔ v x⁻¹ < 1)
This theorem states that for any division ring `K` and any element `x` of `K` that is not zero, along with a valuation `v` from `K` to another type `Γ₀` that is a linearly ordered commutative group with zero, the value `v x` is greater than one if and only if the value `v x⁻¹` is less than one; here `x⁻¹` denotes the multiplicative inverse of `x` in `K`. In other words, this theorem provides a relationship between the valuation of an element and the valuation of its inverse in the context of division rings.
More concisely: For any division ring `K`, element `x` in `K` not equal to zero, and valuation `v` from `K` to a linearly ordered commutative group with zero `Γ₀`, the elements `x` and `x⁻¹` have opposing valuations, i.e., `v x > 1 <-> v (x⁻¹) < 1`.
|
AddValuation.top_iff
theorem AddValuation.top_iff :
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
[inst_2 : Nontrivial Γ₀] (v : AddValuation K Γ₀) {x : K}, v x = ⊤ ↔ x = 0
The theorem `AddValuation.top_iff` states that for any division ring `K` and any type `Γ₀` that is a linear ordered additive commutative monoid with a top element, and a nontrivial instance of `Γ₀`, if `v` is an additive valuation on `K` with values in `Γ₀`, then the valuation `v(x)` of any element `x` of `K` equals the top element if and only if `x` is zero. In mathematical terms, this theorem asserts that in such a setting, the valuation of an element being the top element is equivalent to the element being zero.
More concisely: For any division ring K and additively-ordered commutative monoid Γ₀ with a top element, an additive valuation v on K with values in Γ₀ satisfies v(x) = top if and only if x is the additive identity of K.
|
Valuation.map_neg
theorem Valuation.map_neg :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
(x : R), v (-x) = v x
The theorem `Valuation.map_neg` asserts that for any ring `R` and any linearly ordered commutative group with zero `Γ₀`, the valuation `v` of the negation of an element `x` from the ring `R` is equal to the valuation of `x` itself. In simpler terms, this means that the valuation of a number and its negative are the same in the context of this particular structure.
More concisely: For any ring R and commutative ordered group Γ₀, the valuation function v satisfies v(−x) = v(x) for all x ∈ R.
|
Valuation.map_add_eq_of_lt_left
theorem Valuation.map_add_eq_of_lt_left :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
{x y : R}, v y < v x → v (x + y) = v x
This theorem states that for any ring `R` and any linearly ordered commutative group with zero `Γ₀`, given a valuation `v` from `R` to `Γ₀` and any two elements `x` and `y` from `R`, if the valuation of `y` is less than the valuation of `x`, then the valuation of the sum of `x` and `y` is equal to the valuation of `x`. In mathematical terms, if `v : R → Γ₀` is a valuation and `v(y) < v(x)`, then `v(x + y) = v(x)`.
More concisely: For any valuation `v` from a ring `R` to a linearly ordered commutative group with zero `Γ₀`, if `x`, `y` are in `R` with `v(y) < v(x)`, then `v(x + y) = v(x)`.
|
Valuation.map_mul
theorem Valuation.map_mul :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
(x y : R), v (x * y) = v x * v y
This theorem, `Valuation.map_mul`, states that for any ring `R` and any linear ordered commutative monoid with zero `Γ₀`, and for any valuation `v` from `R` to `Γ₀`, the valuation of the product of two elements `x` and `y` from `R` is equal to the product of the valuations of `x` and `y`. This is a mathematical property that is often associated with valuation maps; it is similar to how a logarithm of a product is the sum of the logarithms.
More concisely: For any ring `R`, commutative monoid with zero `Γ₀`, and valuation `v` from `R` to `Γ₀`, `v (xy) = v x * v y`.
|
Valuation.map_zero
theorem Valuation.map_zero :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
v 0 = 0
The theorem `Valuation.map_zero` states that for any ring `R` and any linearly ordered commutative monoid with zero `Γ₀`, the valuation `v` of the zero element of `R` is always zero. In mathematical terms, this can be expressed as ∀v : Valuation R Γ₀, v(0) = 0. This theorem essentially encapsulates the property of valuations that they map the zero element of a ring to the zero element of the ordered monoid.
More concisely: For any ring R and linearly ordered commutative monoid with zero Γ₀, the valuation map v maps the zero element of R to the zero element of Γ₀, i.e., v(0) = 0.
|
AddValuation.IsEquiv.comap
theorem AddValuation.IsEquiv.comap :
∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
[inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {v₁ : AddValuation R Γ₀}
{v₂ : AddValuation R Γ'₀} {S : Type u_7} [inst_3 : Ring S] (f : S →+* R),
v₁.IsEquiv v₂ → (AddValuation.comap f v₁).IsEquiv (AddValuation.comap f v₂)
The theorem states that if two additive valuations, `v₁` and `v₂`, on a ring `R` are equivalent, then their respective comap (inverse image) under a ring homomorphism `f` from a ring `S` to `R` are also equivalent. This is true for any types `Γ₀` and `Γ'₀` that are linearly ordered additive commutative monoids with a top element. In other words, the operation `comap` preserves the equivalence relation between additive valuations.
More concisely: If `v₁` and `v₂` are equivalent additive valuations on a ring `R`, then their inverse images under a ring homomorphism `f` from a ring `S` to `R` are equivalent.
|
Valuation.map_add
theorem Valuation.map_add :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
(x y : R), v (x + y) ≤ max (v x) (v y)
This theorem states that for any ring `R` and any linearly ordered commutative monoid with zero `Γ₀`, if `v` is a valuation from `R` to `Γ₀`, then the valuation of the sum of any two elements `x` and `y` from `R` is less than or equal to the maximum of the valuations of `x` and `y`. In mathematical terms, this can be written as: for all `x, y ∈ R`, `v(x + y) ≤ max(v(x), v(y))`. This is a property of valuations in valuation theory, a branch of algebra that studies functions that measure 'size' or 'order of magnitude' of elements in a ring.
More concisely: For any ring `R`, any linearly ordered commutative monoid with zero `Γ₀`, and any valuation `v` from `R` to `Γ₀`, `v(x + y) ≤ max(v(x), v(y))` for all `x, y ∈ R`.
|
Valuation.map_add_le
theorem Valuation.map_add_le :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
{x y : R} {g : Γ₀}, v x ≤ g → v y ≤ g → v (x + y) ≤ g
This theorem states that for any ring `R` and any linearly ordered commutative monoid with zero `Γ₀`, given a valuation `v` from `R` to `Γ₀`, and any elements `x`, `y` of `R` and `g` of `Γ₀`, if the valuation of `x` and the valuation of `y` are both less than or equal to `g`, then the valuation of the sum of `x` and `y` is also less than or equal to `g`. In other words, the valuation function preserves the order under addition in the ring.
More concisely: For any ring `R`, linearly ordered commutative monoid with zero `Γ₀`, valuation `v` from `R` to `Γ₀`, and all `x`, `y` in `R` and `g` in `Γ₀`, if `v(x) ≤ g` and `v(y) ≤ g`, then `v(x + y) ≤ g`.
|
Valuation.isEquiv_of_val_le_one
theorem Valuation.isEquiv_of_val_le_one :
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5}
[inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀)
(v' : Valuation K Γ'₀), (∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1) → v.IsEquiv v'
This theorem, `Valuation.isEquiv_of_val_le_one`, states that for any division ring `K` and two types `Γ₀` and `Γ'₀`, which are both linearly ordered commutative groups with zero, if for any element `x` of `K` the valuation `v` of `x` is less than or equal to 1 if and only if the valuation `v'` of `x` is also less than or equal to 1, then the valuations `v` and `v'` are equivalent. In other words, if two valuations agree on whether or not their values are less than or equal to 1 for all elements of the division ring, these two valuations are considered equivalent.
More concisely: If for all `x` in a division ring `K`, the valuations `v` and `v'` satisfy `v x <= 1 <-> v' x <= 1`, then `v` and `v'` are equivalent.
|
Valuation.mem_supp_iff
theorem Valuation.mem_supp_iff :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
(v : Valuation R Γ₀) (x : R), x ∈ v.supp ↔ v x = 0
The theorem `Valuation.mem_supp_iff` states that for any type `R` with a commutative ring structure, any type `Γ₀` with a structure of a linear ordered commutative monoid with zero, a valuation `v` from `R` to `Γ₀`, and an element `x` of `R`, `x` is in the support of the valuation `v` if and only if the valuation `v` of `x` is zero. The support of a valuation `v` is the ideal of `R` where `v` vanishes. In other words, this theorem connects the zero values of a valuation with the elements in its support.
More concisely: For any commutative ring `R`, valuation `v` from `R` to a linear ordered commutative monoid `Γ₀`, and element `x` in `R`, `x` is in the support of `v` if and only if `v(x) = 0`.
|
Valuation.isEquiv_iff_val_le_one
theorem Valuation.isEquiv_iff_val_le_one :
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5}
[inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀)
(v' : Valuation K Γ'₀), v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
This theorem states that for any division ring `K` and any two types `Γ₀` and `Γ'₀`, both of which are linearly ordered commutative groups with zero, any two valuations `v` and `v'` on `K` with values in `Γ₀` and `Γ'₀` respectively are equivalent if and only if for every element `x` of `K`, `v x ≤ 1` if and only if `v' x ≤ 1`. Here, two valuations are considered equivalent if they induce the same preorder on `K`.
More concisely: Two valuations on a division ring with values in linearly ordered commutative groups induce the same preorder on the ring if and only if they agree on the value of every element being less than or equal to 1.
|
ValuationClass.map_add_le_max
theorem ValuationClass.map_add_le_max :
∀ {F : Type u_7} {R : outParam (Type u_5)} {Γ₀ : outParam (Type u_6)} [inst : LinearOrderedCommMonoidWithZero Γ₀]
[inst_1 : Ring R] [inst_2 : FunLike F R Γ₀] [self : ValuationClass F R Γ₀] (f : F) (x y : R),
f (x + y) ≤ max (f x) (f y)
This theorem states that for any types `F`, `R`, and `Γ₀`, where `Γ₀` is a linearly ordered commutative monoid with zero, `R` is a ring, and `F` is a function-like type from `R` to `Γ₀`, if `f` is a function of type `F` and `x` and `y` are elements of `R`, then the valuation (the image under `f`) of the sum of `x` and `y` is less than or equal to the maximum of the valuations of `x` and `y`. The function `f` here can be thought of as a kind of valuation function, and this theorem is expressing a property of it in the context of a ring and a linearly ordered commutative monoid with zero.
More concisely: For any function-like type `F` from a commutative ring `R` to a linearly ordered commutative monoid with zero `Γ₀`, if `f` is a function of type `F` and `x` and `y` are elements of `R`, then `f(x + y) ≤ max(f(x), f(y))`.
|
Valuation.IsEquiv.val_eq
theorem Valuation.IsEquiv.val_eq :
∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
[inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
v₁.IsEquiv v₂ → ∀ {r s : R}, v₁ r = v₁ s ↔ v₂ r = v₂ s
This theorem, `Valuation.IsEquiv.val_eq`, states that for any arbitrary types `R`, `Γ₀`, and `Γ'₀`, where `R` is a ring and `Γ₀`, `Γ'₀` are linear ordered commutative monoids both having a zero element, if two valuations `v₁` and `v₂` on `R` with values in `Γ₀` and `Γ'₀` respectively are equivalent (meaning they induce the same preorder on `R`), then for any two elements `r` and `s` of `R`, `v₁ r = v₁ s` if and only if `v₂ r = v₂ s`. In other words, if two valuations are equivalent, then they agree on when they assign the same valuation to two elements in the ring.
More concisely: If two valuations on a ring with values in commutative monoids having a zero element, inducing the same preorder on the ring, then they agree on the valuation of any two elements in the ring.
|
Valuation.map_eq_of_sub_lt
theorem Valuation.map_eq_of_sub_lt :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
{x y : R}, v (y - x) < v x → v y = v x
The theorem `Valuation.map_eq_of_sub_lt` states that for any type `R`, which is a ring, and any type `Γ₀`, which is a linearly ordered commutative group with zero, and for any valuation `v` of type `R` to `Γ₀`, if the valuation of `(y - x)` is less than the valuation of `x`, then the valuation of `y` is equal to the valuation of `x`. Here, `x` and `y` are any elements of the ring `R`. This theorem captures a particular property of valuation functions in the context of ring theory.
More concisely: If `v` is a valuation from a ring `R` to a linearly ordered commutative group `Γ₀` with zero, then `v(x) ≤ v(y)` implies `v(x) = v(y)` for any `x, y` in `R`.
|
Valuation.map_add_le_max'
theorem Valuation.map_add_le_max' :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] [inst_1 : Ring R]
(self : Valuation R Γ₀) (x y : R), self.toFun (x + y) ≤ max (self.toFun x) (self.toFun y)
This theorem states that for any ring `R` and any linearly ordered commutative monoid with zero `Γ₀`, for any valuation `self` from `R` to `Γ₀`, and for any elements `x` and `y` in `R`, the valuation of the sum of `x` and `y` is less than or equal to the maximum of the valuations of `x` and `y` individually. In simpler terms, the valuation of the sum is never greater than the largest of the individual valuations.
More concisely: For any ring `R`, linearly ordered commutative monoid with zero `Γ₀`, valuation `self` from `R` to `Γ₀`, and elements `x` and `y` in `R`, `self x + self y ≤ max self x self y`.
|
Valuation.isEquiv_iff_val_eq_one
theorem Valuation.isEquiv_iff_val_eq_one :
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5}
[inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀)
(v' : Valuation K Γ'₀), v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1
The theorem `Valuation.isEquiv_iff_val_eq_one` states that for all division rings `K` and for all linearly ordered commutative groups with zero `Γ₀` and `Γ'₀`, a valuation `v` from `K` to `Γ₀` and a valuation `v'` from `K` to `Γ'₀` are equivalent (i.e., they induce the same preorder on `K`) if and only if for all elements `x` in `K`, the valuation `v` of `x` equals 1 if and only if the valuation `v'` of `x` also equals 1.
More concisely: Two valuations from a division ring to linearly ordered commutative groups with zero are equivalent if and only if they assign value 1 to the same elements.
|
Valuation.IsEquiv.comap
theorem Valuation.IsEquiv.comap :
∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
[inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {S : Type u_7}
[inst_3 : Ring S] (f : S →+* R), v₁.IsEquiv v₂ → (Valuation.comap f v₁).IsEquiv (Valuation.comap f v₂)
The theorem `Valuation.IsEquiv.comap` states that if we have two equivalent valuations, `v₁` and `v₂`, on a ring `R`, then their comaps through a ring homomorphism `f` from another ring `S` to `R` are also equivalent. This means that the property of being equivalent for valuations is preserved under the 'comap' operation, which is an operation that maps a valuation on a ring to a valuation on another ring through a ring homomorphism.
More concisely: If `v₁` and `v₂` are equivalent valuations on a ring `R`, then their comaps `f ∘ v₁` and `f ∘ v₂` through a ring homomorphism `f` from another ring `S` to `R` are also equivalent valuations on `S`.
|
Valuation.map_one
theorem Valuation.map_one :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
v 1 = 1
This theorem, named `Valuation.map_one`, states that for any ring `R` of some type `u_3` and any linearly ordered commutative monoid with zero `Γ₀` of some type `u_4`, any valuation `v` of `R` into `Γ₀` will map the multiplicative identity `1` in `R` to the multiplicative identity `1` in `Γ₀`. In other words, it asserts the preservation of the multiplicative identity under the valuation map for these mathematical structures.
More concisely: For any valuation `v` from a ring `R` to a linearly ordered commutative monoid with zero `Γ₀`, `v(1) = 1` holds in `Γ₀`, where `1` refers to the multiplicative identities in `R` and `Γ₀`, respectively.
|
Valuation.ext
theorem Valuation.ext :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
{v₁ v₂ : Valuation R Γ₀}, (∀ (r : R), v₁ r = v₂ r) → v₁ = v₂
This theorem states that for any ring `R` and any linearly ordered commutative monoid with zero `Γ₀`, if two valuations `v₁` and `v₂` from `R` to `Γ₀` map every element of `R` to the same value, then `v₁` and `v₂` are identical. In other words, two valuations are considered equal if they agree on all elements of the ring.
More concisely: Two valuations from a ring to a linearly ordered commutative monoid with zero are equal if and only if they agree on all ring elements.
|
Valuation.map_add_of_distinct_val
theorem Valuation.map_add_of_distinct_val :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
{x y : R}, v x ≠ v y → v (x + y) = max (v x) (v y)
This theorem, `Valuation.map_add_of_distinct_val`, states that for any ring `R` and any linearly ordered commutative group with zero `Γ₀`, given a valuation `v` of `R` into `Γ₀`, and any two elements `x` and `y` of `R` such that the valuation of `x` is not equal to the valuation of `y`, then the valuation of the sum of `x` and `y` is equal to the maximum of the valuations of `x` and `y`. In other words, if the values of `x` and `y` under the valuation `v` are distinct, the valuation of their sum is equal to the greater of the two valuations.
More concisely: For any ring `R`, commutative group with zero `Γ₀`, valuation `v` from `R` to `Γ₀`, and distinct elements `x` and `y` in `R`, `v(x + y) = max {v(x), v(y)}`.
|
Valuation.ext_iff
theorem Valuation.ext_iff :
∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
{v₁ v₂ : Valuation R Γ₀}, v₁ = v₂ ↔ ∀ (r : R), v₁ r = v₂ r
This theorem, `Valuation.ext_iff`, is deprecated and it is recommended to use `DFunLike.ext_iff` instead. The theorem states that for any given ring `R` and any linearly ordered commutative monoid with zero `Γ₀`, two valuations `v₁` and `v₂` from ring `R` to `Γ₀` are equal if and only if they evaluate to the same value for every element `r` of ring `R`.
More concisely: Two valuations from a ring to a linearly ordered commutative monoid with zero are equal if and only if they assign the same value to every ring element.
|
Valuation.zero_iff
theorem Valuation.zero_iff :
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
[inst_2 : Nontrivial Γ₀] (v : Valuation K Γ₀) {x : K}, v x = 0 ↔ x = 0
This theorem states that for any division ring `K` and any value `x` from this division ring, if `v` is a valuation on `K` into a type `Γ₀` (which is a linear ordered commutative monoid with zero where zero is not the only element), then the valuation `v(x)` equals zero if and only if `x` equals zero. This means that a valuation `v` maps zero to zero and only zero to zero in the context of a division ring.
More concisely: For any division ring `K` and valuation `v` on `K` into a linear ordered commutative monoid `Γ₀` with zero, `v(x) = 0` if and only if `x = 0`.
|