| changeset 72671 | 588c751a5eef |
| parent 69785 | 9e326f6f8a24 |
| 72670:4db9411c859c | 72671:588c751a5eef |
|---|---|
8 |
8 |
9 theory Totient |
9 theory Totient |
10 imports |
10 imports |
11 Complex_Main |
11 Complex_Main |
12 "HOL-Computational_Algebra.Primes" |
12 "HOL-Computational_Algebra.Primes" |
13 "~~/src/HOL/Number_Theory/Cong" |
13 Cong |
14 begin |
14 begin |
15 |
15 |
16 definition totatives :: "nat \<Rightarrow> nat set" where |
16 definition totatives :: "nat \<Rightarrow> nat set" where |
17 "totatives n = {k \<in> {0<..n}. coprime k n}" |
17 "totatives n = {k \<in> {0<..n}. coprime k n}" |
18 |
18 |