Unramified algebras over Dedekind domains #
We prove that a domain finite and unramified over a Dedekind domain is a Dedekind domain.
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] :
@[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] :
Alias of IsDedekindDomain.of_formallyUnramified.
@[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] :
Alias of IsDedekindDomain.of_formallyUnramified.