no goals
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type ?u.472756
P2 : Type ?u.472759
V3 : Type ?u.472762
P3 : Type ?u.472765
V4 : Type ?u.472768
P4 : Type ?u.472771
inst✝¹³ : Ring k
inst✝¹² : AddCommGroup V1
inst✝¹¹ : Module k V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : Module k V2
inst✝⁷ : AffineSpace V2 P2
inst✝⁶ : AddCommGroup V3
inst✝⁵ : Module k V3
inst✝⁴ : AffineSpace V3 P3
inst✝³ : AddCommGroup V4
inst✝² : Module k V4
inst✝¹ : AffineSpace V4 P4
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c : k
⊢ ↑(lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]