u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c k : ℕ
a : R
⊢ a ^ (c * k) = (a ^ c) ^ k
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b c k : ℕ
a d e : R
x✝² : b = c * k
x✝¹ : a ^ c = d
x✝ : d ^ k = e
⊢ a ^ b = e
subst_vars
no goals
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c k : ℕ
a : R
⊢ a ^ (c * k) = (a ^ c) ^ k
simp [pow_mul]