Associatehood_is_Equivalence_Relation
Provedassociatesequivalence-relationsintegral-domainsproofwiki
The relation of being associates is an equivalence relation in an integral domain.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Associatehood_is_Equivalence_Relation {D : Type _} [CommMonoidWithZero D] : Reflexive (@Associated D _) ∧ Symmetric (@Associated D _) ∧ Transitive (@Associated D _) := by sorrySource