no goals
R : Type ?u.809738
k : Type u_3
V1 : Type u_2
P1 : Type u_1
V2 : Type ?u.809750
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c : P1
r₁ r₂ : k
p : P1
⊢ ↑(homothety c (r₁ * r₂)) p = ↑(homothety c r₁) (↑(homothety c r₂) p)
simp only [homothety_apply, mul_smul, vadd_vsub]