no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AddTorsor V P
a b : P
⊢ ↑(homothety a (1 / 2)) b = midpoint k a b
rw [one_div, homothety_inv_two]