:: deftheorem Def20 defines the_left_translation_of GROUP_10:def 20 :
for G being finite Group
for p being prime Nat
for H being Subgroup of G
for h being Element of H
for b₅ being Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) holds
( b₅ = the_left_translation_of (h,p) iff for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st
( P2 = b₅ . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) );