| changeset 58860 | fee7cfa69c50 |
| parent 35849 | b5522b51cb1e |
| child 61382 | efac889fccbc |
--- a/src/HOL/Algebra/Module.thy Sat Nov 01 11:40:55 2014 +0100 +++ b/src/HOL/Algebra/Module.thy Sat Nov 01 14:20:38 2014 +0100 @@ -118,7 +118,7 @@ qed lemma (in algebra) smult_r_null [simp]: - "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"; + "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>" proof - assume R: "a \<in> carrier R" note facts = R smult_closed