English
The domain of the unique LinearPMap supported on the span R ∙ x that maps x to y is precisely the span R ∙ x.
Русский
Область определения единственного LinearPMap, опирающегося на пространство, порожденное x, и отправляющего x в y, равна span_R(x).
LaTeX
$$$\\mathrm{dom}(\\mathrm{mkSpanSingleton}'(x,y,H))=\\mathrm{span}_R\\{x\\}$$$
Lean4
/-- The unique `LinearPMap` on `R ∙ x` that sends `x` to `y`. This version works for modules
over rings, and requires a proof of `∀ c, c • x = 0 → c • y = 0`. -/
noncomputable def mkSpanSingleton' (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) : E →ₗ.[R] F
where
domain := R ∙ x
toFun :=
have H : ∀ c₁ c₂ : R, c₁ • x = c₂ • x → c₁ • y = c₂ • y :=
by
intro c₁ c₂ h
rw [← sub_eq_zero, ← sub_smul] at h ⊢
exact H _ h
{ toFun z := Classical.choose (mem_span_singleton.1 z.prop) • y
map_add' y
z := by
rw [← add_smul, H]
have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
simp only [add_smul, this, ← coe_add]
map_smul' c
z := by
rw [smul_smul, H]
have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
simp only [mul_smul, this]
apply coe_smul }
