Theorems · Inductive type · commutative algebra

IsDedekindDomain

(A : Type u_2) → [CommRing A] → Prop

A Dedekind domain is an integral domain that is Noetherian, integrally closed, and has Krull dimension at most one. This is definition 3.2 of [Neukirch1992]. This is exactly IsDedekindRing plus the IsDomain hypothesis. The integral closure condition is independent of the choice of field of fractions: use isDedekindDomain_iff to prove IsDedekindDomain for a given fraction_map. This is the default implementation, but there are equivalent definitions, IsDedekindDomainDvr and IsDedekindDomainInv.

Defined in

Mathlib.RingTheory.DedekindDomain.Basic

Cited by

668 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CommRing