Lines Matching refs:exp
286 and (f*.id = #1) /\ (f*.exp = $** ) by field_nonzero_mult_property
370 so g.exp x (CARD G) = g.id by finite_group_Fermat
371 or f*.exp x k = f*.id by generated_property, generated_exp
446 = IMAGE (\j. f*.exp z j) (count (forder z)) by generated_carrier_as_image
468 BIJ (\n. f*.exp z n) (count (forder z)) (Generated f* z).carrier: thm
1753 <=> p IN g.carrier /\ (g.exp p n = |1|) by roots_of_unity_element
1754 <=> poly p /\ p <> |0| /\ deg p < deg z /\ (g.exp p n = |1|) by poly_mod_ring_nonzero_element, 0 < deg z
1771 `p IN (roots_of_unity g n).carrier <=> p IN g.carrier /\ (g.exp p n = |1|)` by rw[roots_of_unity_element] >>
1772 `_ = (poly p /\ p <> |0| /\ deg p < deg z /\ (g.exp p n = |1|))` by metis_tac[poly_mod_ring_nonzero_element] >>
1879 Z_2 = {0, 1} = {0, exp(i * 2 * pi)} = origin + unity
1893 Z_3 = {0, 1, -1} = {0, exp(i * 2pi/2), exp(i * 2 * 2pi/2)} = {0, -1, (-1)^2 = 1} = origin + dipole
1907 F_4 = {0, 1, w, w^2} = {0, exp(i * 2pi/3), exp(i * 2 * 2pi/3), exp(i * 3 * 2pi/3)} = {0, w, w^2, w^3=1}
1922 Z_5 = {0, 1, -1, i, -i} = {0, exp(i * 2pi/4), exp(i * 2 * 2pi/4), exp(i * 3 * 2pi/4), exp(i * 4 * 2pi/4)}
1936 Z_7 = {0, exp(i * 2pi/6), exp(i * 2 * 2pi/6), exp(i * 3 * 2pi/6), exp(i * 4 * 2pi/6), exp(i * 5 * 2pi/6), exp(i * 6 * 2pi/6)}
1939 F_9 = {0, exp(i * k * 2pi/8) where k = 1, 2, 3, 4, 5, 6, 7, 8} = origin + octagon