Theorems · Theorem · commutative algebra

isDedekindDomain_iff

∀ (A : Type u_2) [inst : CommRing A] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra A K] [IsFractionRing A K],
  IsDedekindDomain A ↔
    IsDomain A ∧ IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, (algebraMap A K) y = x

An integral domain is a Dedekind domain iff and only if it is Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field. In particular, this definition does not depend on the choice of this fraction field.

Defined in

Mathlib.RingTheory.DedekindDomain.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsFractionRing