Kernel support is contained in cokernel support

The only input is the Hopfian property of a finite module over a commutative Noetherian ring. The proof is deliberately made at a prime, using the actual LocalizedModule support definition.

theorem AlgebraicAnalysis.endomorphism_kernel_support_subset_cokernel_support {R : Type u_1} {E : Type u_2} [CommRing R] [AddCommGroup E] [Module R E] [IsNoetherianRing R] [Module.Finite R E] (f : Module.End R E) : Module.support R ↥(LinearMap.ker f) ⊆ Module.support R (E ⧸ LinearMap.range f)