equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Things that can be added to the Algebra library\<close> |
5 section \<open>Things that can be added to the Algebra library\<close> |
6 |
6 |
7 theory Algebra_Aux |
7 theory Algebra_Aux |
8 imports "~~/src/HOL/Algebra/Ring" |
8 imports "HOL-Algebra.Ring" |
9 begin |
9 begin |
10 |
10 |
11 definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where |
11 definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where |
12 "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> = (op \<oplus>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub> ^^ n) \<zero>\<^bsub>R\<^esub>" |
12 "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> = (op \<oplus>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub> ^^ n) \<zero>\<^bsub>R\<^esub>" |
13 |
13 |