Theorems · Definition · commutative algebra

IsDiscreteValuationRing.toEuclideanDomain

(R : Type u_2) → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDiscreteValuationRing R] → EuclideanDomain R

A noncomputable Euclidean domain structure on a discrete valuation ring, where the GCD algorithm only takes two steps to terminate. Given GCD(x,y), if x ∣ y then y%x = 0 so we're done in one step; otherwise y%x = y and then GCD(x,y) = GCD(y,x) which brings us back to the first case. See EuclideanDomain.to_principal_ideal_domain for EuclideanDomain ⇒ PID.

Defined in

Mathlib.RingTheory.DiscreteValuationRing.Basic

Cited by

0 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainIsDiscreteValuationRing