Lines Matching refs:exp
151 = case OLEAST k. 0 < k /\ (f*.exp x k = f*.id) of NONE => 0 | SOME k => k by period_def
165 val it = |- FiniteGroup f* ==> !x. x IN F* ==> 0 < forder x /\ (f*.exp x (forder x) = f*.id): thm
176 val it = |- !x. f*.exp x (forder x) = f*.id: thm
187 val it = |- !x n. 0 < n /\ n < forder x ==> f*.exp x n <> f*.id: thm
235 <=> !n. 0 < n ==> f*.exp #0 n <> f*.id by order_eq_0
248 also !n. f*.exp x n = x ** n by monoid_exp_def
252 val it = |- !x. (forder x = 0) <=> !n. 0 < n ==> f*.exp x n <> f*.id: thm
260 `!n. f*.exp x n = x ** n` by rw[monoid_exp_def] >>
433 val it = |- Group f* ==> !x. x IN F* ==> !n. (f*.exp x n = f*.id) <=> forder x divides n: thm
489 val it = |- Group f* ==> !x. x IN F* ==> !k. forder (f*.exp x k) * gcd (forder x) k = forder x: thm
566 Also !n. *.exp x n = x ** n by group_excluding_exp
571 (forder (f*.exp x (forder x DIV n)) = n): thm