Resolvent set for `linear_pmap`

Stream: maths

[Moritz Doll]

Hi, we have docs#resolvent_set for the resolvent set of a linear_pmap this is useless since linear_pmap is not a ring (not even a monoid, which is needed for units). But the definition would work with some tweaks: units only needs has_mul and for resolvent_set it is only necessary to calculate $\lambda - A$, where $\lambda$ is a complex number and this could be formalized using vadd (vadd is a perfectly reasonable operator for linear_pmap, you can always add multiples of the identity).
The question is whether changing units and resolvent_set is worth the effort, at least for resolvent_set it is probably quite some work and a hack around would be that linear_pmap has it's own resolvent_set definition.