case h
R : Type ?u.815526
k : Type u_3
V1 : Type u_1
P1 : Type u_2
V2 : Type ?u.815538
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c p : P1
⊢ ↑(homothety c 0) p = ↑(const k P1 c) p
R : Type ?u.815526
k : Type u_3
V1 : Type u_1
P1 : Type u_2
V2 : Type ?u.815538
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c : P1
⊢ homothety c 0 = const k P1 c
ext p
no goals
case h
R : Type ?u.815526
k : Type u_3
V1 : Type u_1
P1 : Type u_2
V2 : Type ?u.815538
inst✝⁵ : CommRing k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V1
inst✝ : Module k V2
c p : P1
⊢ ↑(homothety c 0) p = ↑(const k P1 c) p
simp [homothety_apply]