case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
f : M ≃ₗ[R] N
g : M
hg : g ≠ 0
⊢ ↑(map f) (-rayOfNeZero R g hg) = -↑(map f) (rayOfNeZero R g hg)
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
f : M ≃ₗ[R] N
v : Ray R M
⊢ ↑(map f) (-v) = -↑(map f) v
induction' v using Module.Ray.ind with g hg
no goals
case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
f : M ≃ₗ[R] N
g : M
hg : g ≠ 0
⊢ ↑(map f) (-rayOfNeZero R g hg) = -↑(map f) (rayOfNeZero R g hg)
simp