[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x✝ y : M
a b : R
h : a + b = 1
x : M
⊢ a • x + b • x = x
[PROOFSTEP]
rw [← add_smul, h, one_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x y : M
⊢ 2 • x = x + x
[PROOFSTEP]
rw [← one_add_one_eq_two, add_smul, one_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ y : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M₂ →+ M
hf : Injective ↑f
smul : ∀ (c : R) (x : M₂), ↑f (c • x) = c • ↑f x
src✝ : DistribMulAction R M₂ := Injective.distribMulAction f hf smul
c₁ c₂ : R
x : M₂
⊢ ↑f ((c₁ + c₂) • x) = ↑f (c₁ • x + c₂ • x)
[PROOFSTEP]
simp only [smul, f.map_add, add_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ y : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M₂ →+ M
hf : Injective ↑f
smul : ∀ (c : R) (x : M₂), ↑f (c • x) = c • ↑f x
src✝ : DistribMulAction R M₂ := Injective.distribMulAction f hf smul
x : M₂
⊢ ↑f (0 • x) = ↑f 0
[PROOFSTEP]
simp only [smul, zero_smul, f.map_zero]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ y : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ↑f
smul : ∀ (c : R) (x : M), ↑f (c • x) = c • ↑f x
c₁ c₂ : R
x : M₂
⊢ (c₁ + c₂) • x = c₁ • x + c₂ • x
[PROOFSTEP]
rcases hf x with ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ y : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ↑f
smul : ∀ (c : R) (x : M), ↑f (c • x) = c • ↑f x
c₁ c₂ : R
x : M
⊢ (c₁ + c₂) • ↑f x = c₁ • ↑f x + c₂ • ↑f x
[PROOFSTEP]
simp only [add_smul, ← smul, ← f.map_add]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ y : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ↑f
smul : ∀ (c : R) (x : M), ↑f (c • x) = c • ↑f x
x : M₂
⊢ 0 • x = 0
[PROOFSTEP]
rcases hf x with ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ y : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ↑f
smul : ∀ (c : R) (x : M), ↑f (c • x) = c • ↑f x
x : M
⊢ 0 • ↑f x = 0
[PROOFSTEP]
rw [← f.map_zero, ← smul, zero_smul]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M✝ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ y : M✝
R : Type u_9
S : Type u_10
M : Type u_11
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ↑f
hsmul : ∀ (c : R) (x : M), ↑f c • x = c • x
src✝ : DistribMulAction S M := distribMulActionLeft (↑f) hf hsmul
a b : R
x : M
⊢ (↑f a + ↑f b) • x = ↑f a • x + ↑f b • x
[PROOFSTEP]
simp only [← f.map_add, hsmul, add_smul]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M✝ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ y : M✝
R : Type u_9
S : Type u_10
M : Type u_11
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ↑f
hsmul : ∀ (c : R) (x : M), ↑f c • x = c • x
src✝ : DistribMulAction S M := distribMulActionLeft (↑f) hf hsmul
x : M
⊢ 0 • x = 0
[PROOFSTEP]
rw [← f.map_zero, hsmul, zero_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r✝ s✝ : R
x✝ y : M
inst✝ : Semiring S
f : S →+* R
src✝¹ : MulActionWithZero S M := MulActionWithZero.compHom M (RingHom.toMonoidWithZeroHom f)
src✝ : DistribMulAction S M := DistribMulAction.compHom M ↑f
r s : S
x : M
⊢ ↑f (r + s) • x = ↑f r • x + ↑f s • x
[PROOFSTEP]
simp [add_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r✝ s : R
x y : M
src✝ : R →* AddMonoid.End M := DistribMulAction.toAddMonoidEnd R M
r : M
⊢ 0 • r = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r✝ s : R
x✝ y✝ : M
src✝ : R →* AddMonoid.End M := DistribMulAction.toAddMonoidEnd R M
x y : R
r : M
⊢ (x + y) • r = x • r + y • r
[PROOFSTEP]
simp [add_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x y : M
zero_eq_one : 0 = 1
⊢ x = 0
[PROOFSTEP]
rw [← one_smul R x, ← zero_eq_one, zero_smul]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
r✝ s : R✝
x y : M
R : Type u_9
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ r • m + (1 - r) • m = m
[PROOFSTEP]
rw [← add_smul, add_sub_cancel'_right, one_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x
[PROOFSTEP]
rw [smul_sub, Convex.combo_self h]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S : Type u_4
M✝ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
R : Type u_9
inst✝¹ : Semiring R
M : Type u_10
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
⊢ P = Q
[PROOFSTEP]
ext
[GOAL]
case smul.h.h
α : Type u_1
R✝ : Type u_2
k : Type u_3
S : Type u_4
M✝ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
R : Type u_9
inst✝¹ : Semiring R
M : Type u_10
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x✝¹ : R
x✝ : M
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
[PROOFSTEP]
exact w _ _
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x y : M
⊢ -r • x + r • x = 0
[PROOFSTEP]
rw [← add_smul, add_left_neg, zero_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x y : M
⊢ -r • -x = r • x
[PROOFSTEP]
rw [neg_smul, smul_neg, neg_neg]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x✝ y : M
u : Rˣ
x : M
⊢ -u • x = -(u • x)
[PROOFSTEP]
rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x✝ y x : M
⊢ -1 • x = -x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ s✝ : R
x y✝ : M
r s : R
y : M
⊢ (r - s) • y = r • y - s • y
[PROOFSTEP]
simp [add_smul, sub_eq_add_neg]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : AddCommMonoid M := inferInstance
a : M
⊢ (fun z a => ↑z • a) 0 a = 0
[PROOFSTEP]
simpa only [Int.cast_zero] using zero_smul R a
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : AddCommMonoid M := inferInstance
z : ℕ
a : M
⊢ (fun z a => ↑z • a) (Int.ofNat (Nat.succ z)) a = a + (fun z a => ↑z • a) (Int.ofNat z) a
[PROOFSTEP]
simp [add_comm, add_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : AddCommMonoid M := inferInstance
z : ℕ
a : M
⊢ (fun z a => ↑z • a) (Int.negSucc z) a = -(fun z a => ↑z • a) (↑(Nat.succ z)) a
[PROOFSTEP]
simp [← smul_assoc, neg_one_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : AddCommMonoid M := inferInstance
a : M
⊢ -1 • a + a = 0
[PROOFSTEP]
nth_rw 2 [← one_smul R a]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : AddCommMonoid M := inferInstance
a : M
⊢ -1 • a + 1 • a = 0
[PROOFSTEP]
rw [← add_smul, add_left_neg, zero_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : M
⊢ n • b = ↑n • b
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ Nat.zero • b = ↑Nat.zero • b
[PROOFSTEP]
rw [Nat.zero_eq, Nat.cast_zero, zero_smul, zero_smul]
[GOAL]
case succ
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : n • b = ↑n • b
⊢ Nat.succ n • b = ↑(Nat.succ n) • b
[PROOFSTEP]
rw [Nat.succ_eq_add_one, Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module ℕ M
n : ℕ
x : M
⊢ SMul.smul n x = n • x
[PROOFSTEP]
rw [nsmul_eq_smul_cast ℕ n x, Nat.cast_id]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module ℕ M
n : ℕ
x : M
⊢ SMul.smul n x = n • x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Module ℕ M
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Module ℕ M
n : ℕ
⊢ ∀ (m : M), n • m = n • m
[PROOFSTEP]
convert nat_smul_eq_nsmul P n
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : R
y : M
⊢ (Nat.zero • x) • y = Nat.zero • x • y
[PROOFSTEP]
simp only [Nat.zero_eq, zero_smul]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ : ℕ
x : R
y : M
n : ℕ
ih : (n • x) • y = n • x • y
⊢ (Nat.succ n • x) • y = Nat.succ n • x • y
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, add_smul, one_smul, ih]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑(AddMonoidHom.flip (smulAddHom ℤ M)) b =
    AddMonoidHom.comp (↑(AddMonoidHom.flip (smulAddHom R M)) b) (Int.castAddHom R)
[PROOFSTEP]
apply AddMonoidHom.ext_int
[GOAL]
case h1
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑(↑(AddMonoidHom.flip (smulAddHom ℤ M)) b) 1 =
    ↑(AddMonoidHom.comp (↑(AddMonoidHom.flip (smulAddHom R M)) b) (Int.castAddHom R)) 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
h : Module ℤ M
n : ℤ
x : M
⊢ SMul.smul n x = n • x
[PROOFSTEP]
rw [zsmul_eq_smul_cast ℤ n x, Int.cast_id]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
h : Module ℤ M
n : ℤ
x : M
⊢ SMul.smul n x = n • x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
⊢ Module ℤ M
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
P : Module ℤ M
n : ℤ
⊢ ∀ (m : M), n • m = n • m
[PROOFSTEP]
convert int_smul_eq_zsmul P n
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℤ
a : M
⊢ ↑f (↑x • a) = ↑x • ↑f a
[PROOFSTEP]
simp only [← zsmul_eq_smul_cast, map_zsmul]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℕ
a : M
⊢ ↑f (↑x • a) = ↑x • ↑f a
[PROOFSTEP]
simp only [← nsmul_eq_smul_cast, AddMonoidHom.map_nsmul, map_nsmul]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
by_cases hR : (n : R) = 0
[GOAL]
case pos
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
by_cases hS : (n : S) = 0
[GOAL]
case neg
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
by_cases hS : (n : S) = 0
[GOAL]
case pos
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
simp [hR, hS, map_zero f]
[GOAL]
case neg
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
suffices ∀ y, f y = 0 by rw [this, this, smul_zero]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
this : ∀ (y : M), ↑f y = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
rw [this, this, smul_zero]
[GOAL]
case neg
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), ↑f y = 0
[PROOFSTEP]
clear x
[GOAL]
case neg
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
⊢ ∀ (y : M), ↑f y = 0
[PROOFSTEP]
intro x
[GOAL]
case neg
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ ↑f x = 0
[PROOFSTEP]
rw [← inv_smul_smul₀ hS (f x), ← map_nat_cast_smul f R S]
[GOAL]
case neg
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ↑n = 0
hS : ¬↑n = 0
x : M
⊢ (↑n)⁻¹ • ↑f (↑n • x) = 0
[PROOFSTEP]
simp [hR, map_zero f]
[GOAL]
case pos
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
suffices ∀ y, f y = 0 by simp [this]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
this : ∀ (y : M), ↑f y = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
simp [this]
[GOAL]
case pos
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), ↑f y = 0
[PROOFSTEP]
clear x
[GOAL]
case pos
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
⊢ ∀ (y : M), ↑f y = 0
[PROOFSTEP]
intro x
[GOAL]
case pos
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
hR : ¬↑n = 0
hS : ↑n = 0
x : M
⊢ ↑f x = 0
[PROOFSTEP]
rw [← smul_inv_smul₀ hR x, map_nat_cast_smul f R S, hS, zero_smul]
[GOAL]
case neg
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ¬↑n = 0
⊢ ↑f ((↑n)⁻¹ • x) = (↑n)⁻¹ • ↑f x
[PROOFSTEP]
rw [← inv_smul_smul₀ hS (f _), ← map_nat_cast_smul f R S, smul_inv_smul₀ hR]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
z : ℤ
x : M
⊢ ↑f ((↑z)⁻¹ • x) = (↑z)⁻¹ • ↑f x
[PROOFSTEP]
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
[GOAL]
case intro.inl
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ ↑f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • ↑f x
[PROOFSTEP]
rw [Int.cast_Nat_cast, Int.cast_Nat_cast, map_inv_nat_cast_smul _ R S]
[GOAL]
case intro.inr
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ ↑f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • ↑f x
[PROOFSTEP]
simp_rw [Int.cast_neg, Int.cast_Nat_cast, inv_neg, neg_smul, map_neg, map_inv_nat_cast_smul _ R S]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S✝ : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_9
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_10
S : Type u_11
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ ↑f (↑c • x) = ↑c • ↑f x
[PROOFSTEP]
rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul, map_int_cast_smul f R S,
  map_inv_nat_cast_smul f R S]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S : Type u_4
M✝ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
R : Type u_9
M : Type u_10
N : Type u_11
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : Zero N
inst✝² : SMul R M
inst✝¹ : SMul R N
inst✝ : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x✝¹ : R
x✝ : M
h : x✝¹ • x✝ = 0
⊢ x✝¹ • f x✝ = 0
[PROOFSTEP]
rw [← hs, h, h0]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
⊢ c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0
[PROOFSTEP]
rw [Ne.def, smul_eq_zero, not_or]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
⊢ ∀ {c : ℕ} {x : M}, c • x = 0 → c = 0 ∨ x = 0
[PROOFSTEP]
intro c x
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
c : ℕ
x : M
⊢ c • x = 0 → c = 0 ∨ x = 0
[PROOFSTEP]
rw [nsmul_eq_smul_cast R, smul_eq_zero]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
c : ℕ
x : M
⊢ ↑c = 0 ∨ x = 0 → c = 0 ∨ x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
⊢ 2 • v = 0 ↔ v = 0
[PROOFSTEP]
haveI := Nat.noZeroSMulDivisors R M
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
this : NoZeroSMulDivisors ℕ M
⊢ 2 • v = 0 ↔ v = 0
[PROOFSTEP]
simp [smul_eq_zero]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M✝ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R M✝
M : Type u_9
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
⊢ CharZero R
[PROOFSTEP]
refine' ⟨fun m n h => @Nat.cast_injective M _ _ _ _ _⟩
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M✝ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R M✝
M : Type u_9
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n
[PROOFSTEP]
rw [← nsmul_one, ← nsmul_one, nsmul_eq_smul_cast R m (1 : M), nsmul_eq_smul_cast R n (1 : M), h]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
⊢ v = -v ↔ v = 0
[PROOFSTEP]
rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]
[GOAL]
α : Type u_1
R : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
⊢ -v = v ↔ v = 0
[PROOFSTEP]
rw [eq_comm, self_eq_neg R M]
[GOAL]
α : Type u_1
R : Type u_2
k✝ : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module ℚ M
k : ℤ
x : M
h : k • x = 0
⊢ k = 0 ∨ x = 0
[PROOFSTEP]
simpa only [zsmul_eq_smul_cast ℚ k x, smul_eq_zero, Rat.zero_iff_num_zero] using h
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
R : Type u_9
inst✝ : Semiring R
m : ℕ
⊢ m • 1 = ↑m
[PROOFSTEP]
rw [nsmul_eq_mul, mul_one]
[GOAL]
α : Type u_1
R✝ : Type u_2
k : Type u_3
S : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
ι : Type u_8
R : Type u_9
inst✝ : Ring R
m : ℤ
⊢ m • 1 = ↑m
[PROOFSTEP]
rw [zsmul_eq_mul, mul_one]