u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea₁ b : ℕ
a₂ xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea₁ b c₁ : ℕ
a₂ c₂ xa₁ : R
x✝¹ : ea₁ * b = c₁
x✝ : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂
subst_vars
no goals
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea₁ b : ℕ
a₂ xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
simp [_root_.mul_pow, pow_mul]