Email Gateway (Aug 18 2022 at 12:50): Email Gateway (Aug 18 2022 at 12:50):From: barzan stefania <stefania_barzan@yahoo.com>
Hi!
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
Last updated: Nov 21 2024 at 12:39 UTC