English
If finrank_K V = 1, then for any nonzero v ∈ V and any y ∈ V, there exists c ∈ K with c v = y.
Русский
Если размерность пространства равна 1, то для любого ненулевого вектора v и любого y существует скаляр c ∈ K, такой что c v = y.
LaTeX
$$$\operatorname{finrank}_K V = 1 \Rightarrow \forall v \in V\,(v \neq 0) \Rightarrow ∀ y \in V, ∃ c \in K, c v = y$$$
Lean4
/-- In a one-dimensional space, any vector is a multiple of any nonzero vector -/
theorem exists_smul_eq_of_finrank_eq_one (h : finrank K V = 1) {x : V} (hx : x ≠ 0) (y : V) : ∃ (c : K), c • x = y :=
by
have : Submodule.span K { x } = ⊤ :=
by
have : FiniteDimensional K V := .of_finrank_eq_succ h
apply eq_top_of_finrank_eq
rw [h]
exact finrank_span_singleton hx
have : y ∈ Submodule.span K { x } := by rw [this]; exact mem_top
exact mem_span_singleton.1 this
