Divisor_Relation_in_Integral_Domain_is_Transitive
Proveddivisibilityintegral-domainsproofwiki
In an integral domain, the divisibility relation is transitive.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Divisor_Relation_in_Integral_Domain_is_Transitive {D : Type _} [CommRing D] [IsDomain D] (x y z : D) (hxy : x ∣ y) (hyz : y ∣ z) : x ∣ z := by sorrySource