Linear Map

Stream: Is there code for X?

[Peter Nelson]

import Mathlib

example {α ι 𝔽 : Type*} [Field 𝔽] (f : ι ↪ α) : (ι → 𝔽) →ₗ[𝔽] (α → 𝔽) := sorry

I want to map each x : (ι → 𝔽) to the vector v : (α → 𝔽) that satisfies v (f i) = x i for all i : ι and v j = 0 for all j outside the range of f. This should be a linear injection. Is this defined somewhere?

[Peter Nelson]

Never mind - it was Function.ExtendByZero.linearMap.