[isabelle] pow_int

Using the definition of function power from the Group.thy , i need to prove that 
"g\<in> carrier G==> g (^) (a::int)\<otimes> g (^) (b::int) = g (^) (a+b)". Does anyone tried to prove this theorem before? 
or is it even possible to prove it in comm_group? 
thank you!
Stefania Barzan


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.