equal
deleted
inserted
replaced
8 section \<open>Residue rings\<close> |
8 section \<open>Residue rings\<close> |
9 |
9 |
10 theory Residues |
10 theory Residues |
11 imports |
11 imports |
12 Cong |
12 Cong |
13 "HOL-Algebra.More_Group" |
|
14 "HOL-Algebra.More_Ring" |
|
15 "HOL-Algebra.More_Finite_Product" |
|
16 "HOL-Algebra.Multiplicative_Group" |
13 "HOL-Algebra.Multiplicative_Group" |
17 Totient |
14 Totient |
18 begin |
15 begin |
19 |
16 |
20 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" |
17 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" |
353 apply (subst finprod_Union_disjoint) |
350 apply (subst finprod_Union_disjoint) |
354 apply auto |
351 apply auto |
355 apply (metis Units_inv_inv)+ |
352 apply (metis Units_inv_inv)+ |
356 done |
353 done |
357 also have "\<dots> = \<one>" |
354 also have "\<dots> = \<one>" |
358 apply (rule finprod_one) |
355 apply (rule finprod_one_eqI) |
359 apply auto |
356 apply auto |
360 apply (subst finprod_insert) |
357 apply (subst finprod_insert) |
361 apply auto |
358 apply auto |
362 apply (metis inv_eq_self) |
359 apply (metis inv_eq_self) |
363 done |
360 done |