Sum of functions with disjoint supports

Stream: Is there code for X?

[Heather Macbeth]

Is there a lemma saying that a function T with T 0 = 0 is automatically additive when composed with functions of disjoint supports?

import algebra.support

variables {α M N : Type*} [add_monoid M] [add_monoid N]

example {T : M → N} (hT : T 0 = 0) {f g : α → M}
  (hfg : disjoint (function.support f) (function.support g)) (a : α) :
  T (f a + g a) = T (f a) + T (g a) :=
begin
  by_cases ha : a ∈ function.support f,
  { have : g a = 0 := function.nmem_support.mp (set.disjoint_left.mp hfg ha),
    simp [this, hT] },
  { have : f a = 0 := function.nmem_support.mp ha,
    simp [this, hT] },
end

[Yakov Pechersky]

I don't think so. This should probably have a variant phrased for docs#zero_hom