equal
deleted
inserted
replaced
20 record 'a monoid = "'a partial_object" + |
20 record 'a monoid = "'a partial_object" + |
21 mult :: "['a, 'a] \<Rightarrow> 'a" (infixl \<open>\<otimes>\<index>\<close> 70) |
21 mult :: "['a, 'a] \<Rightarrow> 'a" (infixl \<open>\<otimes>\<index>\<close> 70) |
22 one :: 'a (\<open>\<one>\<index>\<close>) |
22 one :: 'a (\<open>\<one>\<index>\<close>) |
23 |
23 |
24 definition |
24 definition |
25 m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" (\<open>inv\<index> _\<close> [81] 80) |
25 m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" |
|
26 (\<open>(\<open>open_block notation=\<open>prefix inv\<close>\<close>inv\<index> _)\<close> [81] 80) |
26 where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G \<and> x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)" |
27 where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G \<and> x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)" |
27 |
28 |
28 definition |
29 definition |
29 Units :: "_ => 'a set" |
30 Units :: "_ => 'a set" |
30 \<comment> \<open>The set of invertible elements\<close> |
31 \<comment> \<open>The set of invertible elements\<close> |