mathlib

f1d5b468 - feat(linear_algebra/basic): add linear_map.eq_locus (#17751)

feat(linear_algebra/basic): add linear_map.eq_locus (#17751) As requested [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/linear_map.2Eeq_locus/near/274852028) by me a while ago.