exponents.thy

theory Exponents
imports Main
begin

lemma rMulComm: "(a*b ::int) = (b*a ::int)"
by (rule Groups.ab_semigroup_mult_class.mult.commute)

lemma rExpMul: "((a^b)^c ::int) = (a^(b*c) ::int)"
by (rule Int.zpower_zpower)

theorem "((a^b)^c ::int) = ((a^c)^b :: int)"
(*  0.  (a^b)^c 
    1.  a^(b*c)   by rExpMul
    2.  a^(c*b)   by rMulComm
    3.  (a^c)^b   by rExpMul
*)
  
end