Unramified algebras over Dedekind domains

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

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] : IsDedekindDomainDvr B

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

A domain finite and unramified over a Dedekind domain is a Dedekind domain.