linear_map.eq_locus

Stream: Is there code for X?

[Eric Wieser]

We have docs#ring_hom.eq_locus and docs#monoid_hom.eq_locus, and even docs#linear_pmap.eq_locus. Unless I'm missing something, is there a reason we don't have docs#linear_map.eq_locus?

[Eric Wieser]

Is it hiding somewhere with a different name?

[Reid Barton]

maybe the kernel of f - g?

[Eric Wieser]

Indeed, but (f - g).ker isn't valid when M is only an additive monoid

[Eric Wieser]

(and is definitionally worse)