Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment