English
Two nonzero vectors determine the same projective point iff one is a scalar multiple of the other, i.e. there exists a ∈ K^× with v = a·w.
Русский
Два ненулевых вектора определяют одну и ту же точку проективного пространства тогда и только тогда, когда один из них является скалярным кратным другого, то есть существует a ∈ K^× с v = a·w.
LaTeX
$$$ mk\ K\ v\ hv = mk\ K\ w\ hw \iff \exists a : K^×, a \cdot w = v $$$
Lean4
/-- Two nonzero vectors go to the same point in projective space if and only if one is
a scalar multiple of the other. -/
theorem mk_eq_mk_iff' (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w hw ↔ ∃ a : K, a • w = v :=
by
rw [mk_eq_mk_iff K v w hv hw]
constructor
· rintro ⟨a, ha⟩
exact ⟨a, ha⟩
· rintro ⟨a, ha⟩
refine ⟨Units.mk0 a fun c => hv.symm ?_, ha⟩
rwa [c, zero_smul] at ha
