Lines Matching refs:exp
125 generated_exp |- !g a z. a IN G /\ z IN Gen a ==> !n. (gen a).exp z n = z ** n
166 Generated_subset_exp |- !g s. (gen_set s).exp = $**
500 `!x. x IN H ==> !n. h.exp x n = x ** n` by metis_tac[subgroup_exp] >>
590 ((Invertibles g).exp x (order (Invertibles g) x) = (Invertibles g).id): thm
598 (Invertibles g).exp x (order (Invertibles g) x) =
602 and (Invertibles g).exp = $** by Invertibles_property
687 (* Theorem: !a. a IN G ==> (Gen a = IMAGE (g.exp a) univ(:num)) *)
691 ``!(g:'a group) a. a IN G ==> (Gen a = IMAGE (g.exp a) univ(:num))``,
830 (* Theorem: a IN G /\ z IN (Gen a) ==> !n. (gen a).exp z n = z ** n *)
832 (gen a).exp z n
835 = g.exp z n by monoid_exp_def
840 ``!g:'a group. !a z. a IN G /\ z IN (Gen a) ==> !n. (gen a).exp z n = z ** n``,
942 ==> (gen a).exp x (CARD (Gen a)) = (gen a).id
945 and !n. (gen a).exp x n = x ** n by generated_exp
955 `!n. (gen a).exp x n = x ** n` by rw[generated_exp] >>
1281 ``!(g:'a group) s. (gen_set s).exp = g.exp``,