k : Type u₁
G : Type u₂
R : Type ?u.1939465
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
⊢ 1 = single 0 1
k : Type u₁
G : Type u₂
R : Type ?u.1939465
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
⊢ single a b ^ 0 = single (0 • a) (b ^ 0)
simp only [pow_zero, zero_nsmul]
no goals
k : Type u₁
G : Type u₂
R : Type ?u.1939465
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
⊢ 1 = single 0 1
rfl
no goals
k : Type u₁
G : Type u₂
R : Type ?u.1939465
inst✝¹ : Semiring k
inst✝ : AddMonoid G
a : G
b : k
n : ℕ
⊢ single a b ^ (n + 1) = single ((n + 1) • a) (b ^ (n + 1))
rw [pow_succ, pow_succ, single_pow n, single_mul_single, add_comm, add_nsmul, one_nsmul]