no goals
k : Type u_2
E : Type u_1
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ slope f a a = 0
rw [slope, sub_self, inv_zero, zero_smul]