Structures · Algebra
IsDedekindRing
A Dedekind ring is a commutative ring that is Noetherian, integrally closed, and
has Krull dimension at most one.
This is exactly IsDedekindDomain minus the IsDomain hypothesis.
The integral closure condition is independent of the choice of field of fractions:
use isDedekindRing_iff to prove IsDedekindRing for a given fraction_map.
- Defined in
- Mathlib.RingTheory.DedekindDomain.Basic
- Shape
- One type argument
Extends3
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…