Extending the linear map with a new vector

Stream: Is there code for X?

[Weiyi Wang]

Before I code up the boilerplate, do we have this in mathlib? (Might need to strengthen some hypothesis on R M and N. I am working with Field R and AddCommGroup M N anyway)

/- Returns a larger linear map F such that F v = fv, and F x = f x for x ∈ m  -/
noncomputable
def LinearMap.extend {R M N : Type*} [Semiring R] [AddCommMonoid M] [AddCommMonoid N]
    [Module R M] [Module R N]
    {m : Submodule R M} (f : ↥m →ₗ[R] N) {v : M} (hv : v ∉ m) (fv : N):
    ↥(m ⊔ R ∙ v : Submodule R M) →ₗ[R] N := sorry

[Weiyi Wang]

Oh, maybe I should use LinearPMap's API

[Weiyi Wang]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/LinearPMap.html#LinearPMap.sup looks like the one I want

[Weiyi Wang]

Oh there is actually LinearPMap.supSpanSingleton ... don't know why it takes so much effort to find

[Weiyi Wang]

Following up on this, it doesn't look like there is an iSup analog on LinearPMap which takes a (infinite) family of maps whose domains are linearly independent. I guess I need to code up some boilerplate after all