no goals
α : Type u_1
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✝ : AddCommGroupWithOne α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = 0 • ↑n
simp
no goals
α : Type u_1
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✝ : AddCommGroupWithOne α
m k : ℤ
x✝ : 0 ≤ k
ih : ∀ (n : ℤ), ↑(k * n) = k • ↑n
n : ℤ
⊢ ↑((k + 1) * n) = (k + 1) • ↑n
simp [add_mul, add_zsmul, ih]
no goals
α : Type u_1
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✝ : AddCommGroupWithOne α
m k : ℤ
x✝ : k ≤ 0
ih : ∀ (n : ℤ), ↑(k * n) = k • ↑n
n : ℤ
⊢ ↑((k - 1) * n) = (k - 1) • ↑n
simp [sub_mul, sub_zsmul, ih, ← sub_eq_add_neg]