dvd_norm

import Mathlib

theorem dvd_norm {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [Module.IsTorsionFree A B] (b : B) (hb : b ≠ 0) : ∃ a : A, a ≠ 0 ∧ b ∣ algebraMap A B a := ⟨Algebra.intNorm A B b, Algebra.intNorm_ne_zero.mpr hb, Algebra.dvd_algebraMap_intNorm_self A B b⟩