no goals
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.37832
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h : SameRay R x y
hx : x = 0
⊢ ↑f x = 0
rw [hx, map_zero]
no goals
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.37832
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ ↑f y = 0
rw [hy, map_zero]
no goals
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.37832
inst✝ : DecidableEq ι
x y z : M
f : M →ₗ[R] N
h✝ : SameRay R x y
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ r₁ • ↑f x = r₂ • ↑f y
rw [← f.map_smul, ← f.map_smul, h]