∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [inst_3 : DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)]
  [∀ (i : ι), Module.Free R ↥(N i)],
  DirectSum.IsInternal N →
    ∀ [IsNoetherian R M] (σ : ι → ι),
      (∀ (i : ι), σ i ≠ i) →
        ∀ {f : Module.End R M}, (∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N (σ i))) → (LinearMap.trace R M) f = 0