DiscreteValuationRing.of_ufd_of_unique_irreducible
theorem DiscreteValuationRing.of_ufd_of_unique_irreducible :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : UniqueFactorizationMonoid R],
(∃ p, Irreducible p) → (∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) → DiscreteValuationRing R
The theorem states that for any commutative ring `R`, which is also a domain and a unique factorization monoid, if there exists at least one irreducible element and all irreducible elements in `R` are associated (that is, any irreducible element can be expressed as a multiplication of another irreducible element and a unit), then `R` is a discrete valuation ring.
In other words, this theorem provides a condition under which a unique factorization domain with at least one irreducible element can be classified as a discrete valuation ring. This condition is that all irreducible elements in the domain are associated.
More concisely: If `R` is a commutative domain in Lean 4 that is a unique factorization monoid with at least one irreducible element and all irreducible elements are associated, then `R` is a discrete valuation ring.
|
DiscreteValuationRing.not_isField
theorem DiscreteValuationRing.not_isField :
∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DiscreteValuationRing R], ¬IsField R
The theorem `DiscreteValuationRing.not_isField` states that for any type `R` that is a commutative ring and a domain, if `R` is a discrete valuation ring, then `R` cannot be a field. This means that no discrete valuation ring can have the full properties of a field, which includes having an additive and multiplicative identity, being closed under addition and multiplication, and every non-zero element having a multiplicative inverse.
More concisely: A discrete valuation ring is not a field.
|
DiscreteValuationRing.associated_pow_irreducible
theorem DiscreteValuationRing.associated_pow_irreducible :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DiscreteValuationRing R] {x : R},
x ≠ 0 → ∀ {ϖ : R}, Irreducible ϖ → ∃ n, Associated x (ϖ ^ n)
This theorem states that for any commutative ring `R`, which is also a domain and a discrete valuation ring, and for any given non-zero element `x` of `R`, if `ϖ` is an irreducible element of `R`, then there exists an integer `n` such that `x` is associated with the `n`-th power of `ϖ`. Here, two elements are said to be associated if one can be obtained by multiplying the other by a unit.
More concisely: For any commutative domain and discrete valuation ring `R` with non-zero element `x` and irreducible element `ϖ`, there exists an integer `n` such that `x` is associated with `ϖ^n`.
|
DiscreteValuationRing.exists_irreducible
theorem DiscreteValuationRing.exists_irreducible :
∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DiscreteValuationRing R], ∃ ϖ, Irreducible ϖ
This theorem states that for any type `R` that is a commutative ring, a domain, and a discrete valuation ring (DVR), there exists an irreducible element `ϖ`. In more mathematical terms, the theorem proves that there's always an irreducible element in any discrete valuation ring, which is a specific type of ring in algebra where elements can be uniquely factorized.
More concisely: In any commutative ring `R` that is a domain and a discrete valuation ring, there exists an irreducible element.
|
DiscreteValuationRing.exists_prime
theorem DiscreteValuationRing.exists_prime :
∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DiscreteValuationRing R], ∃ ϖ, Prime ϖ := by
sorry
This theorem states that for every Discrete Valuation Ring (DVR) `R`, which is a commutative ring and an integral domain, there exists an element `ϖ` that is prime. In the context of DVRs, a prime element is one that is not zero, not a unit, and for any two elements `a` and `b` in the ring, if the prime element divides the product of `a` and `b`, then it must divide either `a` or `b`.
More concisely: Every Discrete Valuation Ring (DVR) is a principal ideal domain, i.e., there exists a prime element `ϖ` such that every ideal in `R` is principal and generated by `ϖ`.
|
DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid
theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid :
∀ {R : Type u_1} [inst : CommRing R],
DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R →
∀ [inst_1 : IsDomain R], UniqueFactorizationMonoid R
The theorem `DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid` states that for any commutative ring `R` that is also an integral domain, if there exists an irreducible element `p` in `R` such that every non-zero element in `R` is associated to some power of `p` (i.e., `R` has the property `DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization`), then `R` is a unique factorization domain. In other words, in such a ring `R`, every non-zero element can be uniquely expressed as a product of irreducible elements (up to order and units), which is the definition of a unique factorization domain.
More concisely: In a commutative integral domain `R` where every non-zero element is associated to some power of an irreducible element `p`, `R` is a unique factorization domain.
|
DiscreteValuationRing.irreducible_iff_uniformizer
theorem DiscreteValuationRing.irreducible_iff_uniformizer :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DiscreteValuationRing R] (ϖ : R),
Irreducible ϖ ↔ LocalRing.maximalIdeal R = Ideal.span {ϖ}
This theorem states that for any element `ϖ` in a Discrete Valuation Ring `R`, `ϖ` is irreducible if and only if it generates the maximal ideal of `R`. In other words, the maximal ideal of `R` is the ideal spanned by the set only containing `ϖ`. This condition is equivalent to `ϖ` being a uniformizer which is a generator of the maximal ideal in a local ring. This theorem bridges the concepts of irreducibility and uniformizers in the context of Discrete Valuation Rings.
More concisely: In a Discrete Valuation Ring, an element is irreducible if and only if it generates the maximal ideal.
|
DiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization
theorem DiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R],
DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R → DiscreteValuationRing R
The theorem `DiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization` states that for any type `R` which has a commutative ring structure and is an integral domain, if `R` satisfies the condition `DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization`, which means there exists an irreducible element `p` in `R` such that every nonzero element in `R` is associated with a power of `p`, then `R` is a discrete valuation ring.
More concisely: If a commutative ring `R` is an integral domain satisfying `DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization` for some irreducible element `p`, then `R` is a discrete valuation ring.
|
DiscreteValuationRing.iff_pid_with_one_nonzero_prime
theorem DiscreteValuationRing.iff_pid_with_one_nonzero_prime :
∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R],
DiscreteValuationRing R ↔ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime
This theorem states that for any commutative ring `R` that is also an integral domain, `R` is a Discrete Valuation Ring (DVR) if and only if it is a Principal Ideal Ring (PID) and there exists exactly one prime ideal `P` in `R` that is not the zero ideal.
More concisely: A commutative ring `R` is a Discrete Valuation Ring if and only if it is both a Principal Ideal Ring and has exactly one non-zero prime ideal.
|