Finitely supported function

Stream: mathlib4

[Seb Roach]

Hi, I have a finitely supported map for the coefficients of a linear combination of vectors. Its domain is Sum A Unit, and I want to restrict it to just A. This is so I can use the restriction (also a finitely supported function) to define the linear combination of a subfamily of vectors, with one less vector. Any ideas how to proceed?

[Kevin Buzzard]

The best way to proceed is for you to ask your question in Lean with a #mwe .

[Seb Roach]

Thank you, its all good now

[Eric Wieser]

Resolved at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Finitely.20supported.20restriction/near/496595528. Please don't post the same question in multiple places in future