equal
deleted
inserted
replaced
29 *) |
29 *) |
30 |
30 |
31 section \<open>Greatest common divisor and least common multiple\<close> |
31 section \<open>Greatest common divisor and least common multiple\<close> |
32 |
32 |
33 theory GCD |
33 theory GCD |
34 imports Groups_List |
34 imports Groups_List Code_Numeral |
35 begin |
35 begin |
36 |
36 |
37 subsection \<open>Abstract bounded quasi semilattices as common foundation\<close> |
37 subsection \<open>Abstract bounded quasi semilattices as common foundation\<close> |
38 |
38 |
39 locale bounded_quasi_semilattice = abel_semigroup + |
39 locale bounded_quasi_semilattice = abel_semigroup + |