ValuationSubring.image_maximalIdeal
theorem ValuationSubring.image_maximalIdeal :
∀ {K : Type u} [inst : Field K] {A : ValuationSubring K},
Subtype.val '' ↑(LocalRing.maximalIdeal ↥A) = ↑A.nonunits
The theorem `ValuationSubring.image_maximalIdeal` states that for any field `K` and for any valuation subring `A` of `K`, the image of the maximal ideal of `A` under the function `Subtype.val` (which takes an element of a subtype and returns the corresponding element in the base type) is equal to the set of non-invertible elements of `A`. In other words, it asserts that the set of elements in `A` that are not units is exactly the image of the maximal ideal of `A` when we view the elements of this ideal as elements of the field `K`.
More concisely: The maximal ideal of a valuation subring maps to the set of non-invertible elements in the base field.
|
ValuationSubring.coe_mem_nonunits_iff
theorem ValuationSubring.coe_mem_nonunits_iff :
∀ {K : Type u} [inst : Field K] {A : ValuationSubring K} {a : ↥A},
↑a ∈ A.nonunits ↔ a ∈ LocalRing.maximalIdeal ↥A
This theorem is about the relationship between the nonunits of a valuation subring and its corresponding maximal ideal. Specifically, for any field `K` and any element `a` of the valuation subring `A` of `K`, the theorem states that `a` is a nonunit of `A` if and only if `a` is in the maximal ideal of `A`. Note that this theorem also involves a type coercion from `A` to `K`, which is a technical detail often encountered in formalizations of algebraic structures. There is also a related theorem called `mem_nonunits_iff_exists_mem_maximalIdeal`, which provides a similar characterization of nonunits without the need for type coercion.
More concisely: For any field `K` and its valuation subring `A`, an element `a` in `A` is a nonunit if and only if it belongs to the maximal ideal of `A`.
|
Mathlib.RingTheory.Valuation.ValuationSubring._auxLemma.7
theorem Mathlib.RingTheory.Valuation.ValuationSubring._auxLemma.7 :
∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (a = b) = (a ≤ b ∧ b ≤ a)
This theorem states that for any type `α` that has a partial order, and for any two elements `a` and `b` of this type, `a` is equal to `b` if and only if `a` is less than or equal to `b` and `b` is less than or equal to `a`. In other words, in a partially ordered set, two elements are equal if they are mutually less than or equal to each other.
More concisely: In a partially ordered set, two elements are equal if and only if they mutually satisfy the relation x ≤ y and y ≤ x.
|
ValuationSubring.coe_mem_principalUnitGroup_iff
theorem ValuationSubring.coe_mem_principalUnitGroup_iff :
∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) {x : ↥A.unitGroup},
↑x ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map ↑(LocalRing.residue ↥A)).ker
This theorem states that for any field `K` and a valuation subring `A` of `K`, a unit `x` from the unit group of `A` belongs to the principal unit group of `A` if and only if the equivalent element of `x` under the unit group multiplication equivalence relation of `A` belongs to the kernel of the monoid homomorphism induced by mapping units of the residue field of `A`. In simpler terms, it relates the elements of the principal unit group and the elements that become identity when mapped to the residue field of the valuation subring.
More concisely: A unit in a valuation subring belongs to its principal unit group if and only if its class under the unit group equivalence relation maps to the identity element in the residue field under the homomorphism of unit groups.
|
ValuationSubring.le_ofPrime
theorem ValuationSubring.le_ofPrime :
∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P : Ideal ↥A) [inst_1 : P.IsPrime], A ≤ A.ofPrime P := by
sorry
The theorem `ValuationSubring.le_ofPrime` states that for any field `K`, valuation subring `A` of the field `K` and a prime ideal `P` of the subring `A`, the valuation subring `A` is a subset of the valuation subring associated to the prime ideal `P`. In other words, this theorem establishes an order relationship between a valuation subring and the coarsening of this valuation ring associated to a prime ideal in that subring.
More concisely: For any field `K`, valuation subring `A` of `K`, and prime ideal `P` of `A`, `A` is included in the valuation subring associated to `P`.
|
ValuationSubring.monotone_mapOfLE
theorem ValuationSubring.monotone_mapOfLE :
∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S), Monotone ⇑(R.mapOfLE S h)
The theorem `ValuationSubring.monotone_mapOfLE` states that for any field `K` and two valuation subrings `R` and `S` of `K` such that `R` is less than or equal to `S`, the canonical map on value groups induced by the coarsening of valuation rings, represented by the function `ValuationSubring.mapOfLE R S h`, is monotone. In other words, if `a` and `b` are any two elements from the value group of `R` such that `a ≤ b`, then the image of `a` under the map is less than or equal to the image of `b`.
More concisely: For any fields K and valuation subrings R ≤ S of K, the map on value groups induced by the coarsening of R to S, ValuationSubring.mapOfLE R S h, is monotone.
|
Mathlib.RingTheory.Valuation.ValuationSubring._auxLemma.4
theorem Mathlib.RingTheory.Valuation.ValuationSubring._auxLemma.4 :
∀ {K : Type u} [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
(x : K), (x ∈ v.valuationSubring) = (v x ≤ 1)
This theorem states that for any field `K`, any linearly ordered commutative group with zero `Γ`, any valuation `v` of the field `K` with values in `Γ`, and any element `x` of the field `K`, `x` is in the valuation subring associated with the valuation `v` if and only if the valuation of `x` is less than or equal to 1. In mathematical notation, this is saying that $x \in \text{Valuation.valuationSubring} \, v$ if and only if $v(x) \leq 1$.
More concisely: A field element `x` belongs to the valuation subring of a valuation `v` if and only if the valuation `v` of `x` is less than or equal to 1.
|
ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal
theorem ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal :
∀ {K : Type u} [inst : Field K] {A : ValuationSubring K} {a : K},
a ∈ A.nonunits ↔ ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ LocalRing.maximalIdeal ↥A
This theorem states that for any field `K` and a valuation subring `A` of `K`, an element `a` in `K` belongs to the set of non-unit elements of `A` if and only if `a` is in `A` and the singleton set containing `a` belongs to the maximal ideal of `A`. In other words, it provides a characterization of non-unit elements of a valuation subring in terms of belonging to the maximal ideal.
More concisely: An element in a field lies in the maximal ideal of a valuation subring if and only if it is a non-unit in the subring.
|
Mathlib.RingTheory.Valuation.ValuationSubring._auxLemma.2
theorem Mathlib.RingTheory.Valuation.ValuationSubring._auxLemma.2 :
∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), (x ∈ A.toSubring) = (x ∈ A)
This theorem states that for any field `K` and any element `x` in `K`, the element `x` belongs to the valuation subring `A` of `K` if and only if `x` belongs to the subring generated by `A`. Here, a valuation subring `A` of a field `K` is a subring that is closed under valuation, meaning that for any `x` in `K`, either `x` or its inverse (if it exists) belongs to `A`.
More concisely: A field element `x` belongs to the valuation subring `A` of a field `K` if and only if it is contained in the subring generated by `A`.
|
ValuationSubring.mem_of_valuation_le_one
theorem ValuationSubring.mem_of_valuation_le_one :
∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), A.valuation x ≤ 1 → x ∈ A
This theorem states that for any field `K` and any valuation subring `A` of `K`, if the valuation of an element `x` from `K` under the valuation induced by `A` is less than or equal to one, then `x` belongs to the valuation subring `A`. In other words, it asserts that any element in the field `K` whose valuation, as defined by the valuation subring `A`, is at most one is actually a member of the valuation subring `A`.
More concisely: If `A` is a valuation subring of the field `K`, then for all `x` in `K` with valuation less than or equal to 1 under the valuation induced by `A`, we have `x` in `A`.
|
ValuationSubring.valuation_le_one_iff
theorem ValuationSubring.valuation_le_one_iff :
∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), A.valuation x ≤ 1 ↔ x ∈ A
This theorem states that for any field `K` and any valuation subring `A` of `K`, and for any element `x` of `K`, the valuation of `x` with respect to `A` is less than or equal to 1 if and only if `x` belongs to `A`. This provides a way to determine whether an element of `K` belongs to a particular valuation subring based on its valuation.
More concisely: For any field `K`, valuation subring `A`, and element `x` in `K`, `x` lies in `A` if and only if the valuation of `x` with respect to `A` is less than or equal to 1.
|
ValuationSubring.mem_or_inv_mem
theorem ValuationSubring.mem_or_inv_mem :
∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : K), x ∈ A ∨ x⁻¹ ∈ A
This theorem states that for any field `K` and any `ValuationSubring A` of `K`, and for any element `x` from `K`, either `x` is a member of `A` or its multiplicative inverse `x⁻¹` is a member of `A`. This means that in any given valuation subring of a field, every element or its reciprocal must be present.
More concisely: For any field `K` and its valuation subring `A`, every element `x` in `K` or its multiplicative inverse `x⁻¹` belongs to `A`.
|
ValuationSubring.valuation_le_one
theorem ValuationSubring.valuation_le_one :
∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A), A.valuation ↑a ≤ 1
This theorem states that for any field `K` and any valuation subring `A` of `K`, the valuation of any element `a` from the valuation subring `A`, under the natural valuation induced by `A` on `K`, is less than or equal to one. In mathematical terms, if `K` is a field and `A` is a valuation subring of `K`, then for all `a` in `A`, the valuation of `a` in `K` (denoted as `(ValuationSubring.valuation A) ↑a`) is less than or equal to 1.
More concisely: For any field `K` and its valuation subring `A`, the valuation of every element `a` in `A` under the induced valuation on `K` is less than or equal to 1.
|