equal
deleted
inserted
replaced
95 qed |
95 qed |
96 |
96 |
97 lemma orbit_cycle_elem: |
97 lemma orbit_cycle_elem: |
98 assumes "distinct as" and "a \<in> set as" |
98 assumes "distinct as" and "a \<in> set as" |
99 shows "orbit \<langle>as\<rangle> a = set as" |
99 shows "orbit \<langle>as\<rangle> a = set as" |
100 oops -- \<open>(we need rotation here\<close> |
100 oops \<comment> \<open>(we need rotation here\<close> |
101 |
101 |
102 lemma order_cycle_elem: |
102 lemma order_cycle_elem: |
103 assumes "distinct as" and "a \<in> set as" |
103 assumes "distinct as" and "a \<in> set as" |
104 shows "order \<langle>as\<rangle> a = length as" |
104 shows "order \<langle>as\<rangle> a = length as" |
105 oops |
105 oops |