Linearity of extension by zero into vanishing modules

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZeroToVanishing_additive {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (finiteDimensionalModuleExtensionByZeroToVanishing C S).Additive

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZeroToVanishing_linear {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : CategoryTheory.Functor.Linear k (finiteDimensionalModuleExtensionByZeroToVanishing C S)

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZeroVanishingEquivalence_additive {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : (finiteDimensionalModuleExtensionByZeroVanishingEquivalence C S).functor.Additive

instance MagnitudeConjecture.ObjectDeletion.finiteDimensionalModuleExtensionByZeroVanishingEquivalence_linear {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) : CategoryTheory.Functor.Linear k (finiteDimensionalModuleExtensionByZeroVanishingEquivalence C S).functor