no goals
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ ↑(of A 0) (a ^ 0) = ↑(of A 0) a ^ 0
rw [pow_zero, pow_zero, DirectSum.of_zero_one]
no goals
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
n : ℕ
⊢ ↑(of A 0) (a ^ (n + 1)) = ↑(of A 0) a ^ (n + 1)
rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]