case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.184783
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.184783
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
v : Ray R M
⊢ -u • v = -(u • v)
induction v using Module.Ray.ind
no goals
case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.184783
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)
simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]