no goals
α : Type ?u.276006
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
a : R
n : ℕ
⊢ ↑n • a = ↑↑n * a
rw [coe_nat_zsmul, nsmul_eq_mul, Int.cast_ofNat]
no goals
α : Type ?u.276006
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Ring R
a : R
n : ℕ
⊢ -[n+1] • a = ↑-[n+1] * a
simp [Nat.cast_succ, neg_add_rev, Int.cast_negSucc, add_mul]