Documentation

Mathlib.RingTheory.Unramified.Dedekind

Unramified algebras over Dedekind domains #

We prove that a domain finite and unramified over a Dedekind domain is a Dedekind domain.

source
theorem IsDedekindDomain.of_formallyUnramified (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B] [IsDedekindDomain A] [IsDomain B] [Algebra.FormallyUnramified A B] :
IsDedekindDomain B
source
@[deprecated IsDedekindDomain.of_formallyUnramified (since := "2026-08-01")]
theorem isDedekindDomainDvr.of_formallyUnramified (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B] [IsDedekindDomain A] [IsDomain B] [Algebra.FormallyUnramified A B] :
IsDedekindDomain B

Alias of IsDedekindDomain.of_formallyUnramified.

source
@[deprecated IsDedekindDomain.of_formallyUnramified (since := "2026-08-01")]
theorem isDedekindDomain.of_formallyUnramified (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B] [IsDedekindDomain A] [IsDomain B] [Algebra.FormallyUnramified A B] :
IsDedekindDomain B

Alias of IsDedekindDomain.of_formallyUnramified.