English
In the division-ring setting, mkSpanSingleton x y hx maps ⟨x, mem_span_singleton_self x⟩ to y, i.e., it sends the canonical representative to y when hx ensures x ≠ 0.
Русский
В случае делимости, mkSpanSingleton x y hx отображает ⟨x, mem_span_singleton_self x⟩ в y; т.е. отправляет канонический представитель в y при hx, гарантирующем x ≠ 0.
LaTeX
$$$\\mathrm{mkSpanSingleton}(x,y,hx)\\langle x, m\\rangle = y\\quad (m = \\mathrm{mem\\_span\\_singleton\\_self}\,x)$$$
Lean4
/-- The unique `LinearPMap` on `span R {x}` that sends a non-zero vector `x` to `y`.
This version works for modules over division rings. -/
noncomputable abbrev mkSpanSingleton {K E F : Type*} [DivisionRing K] [AddCommGroup E] [Module K E] [AddCommGroup F]
[Module K F] (x : E) (y : F) (hx : x ≠ 0) : E →ₗ.[K] F :=
mkSpanSingleton' x y fun c hc => (smul_eq_zero.1 hc).elim (fun hc => by rw [hc, zero_smul]) fun hx' => absurd hx' hx
