equal
deleted
inserted
replaced
809 by (rule unit_mult_right_cancel) |
809 by (rule unit_mult_right_cancel) |
810 with assms show ?thesis by simp |
810 with assms show ?thesis by simp |
811 qed |
811 qed |
812 |
812 |
813 |
813 |
814 text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close> |
814 text \<open>Associated elements in a ring --- an equivalence relation induced |
|
815 by the quasi-order divisibility.\<close> |
815 |
816 |
816 definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
817 definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
817 where |
818 where |
818 "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a" |
819 "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a" |
819 |
820 |