@[reducible, inline]

abbrev CategoryTheory.Proposition_2_10_7_part1 {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [LeftModuleCategory C M] (h : InternalHomExactInSecondVar C M) : ExactModuleCategory C M

Proposition 2.10.7 (EGNO), part 1: A module category M over C is exact whenever the internal Hom is exact in its second variable.

@[reducible]

noncomputable def CategoryTheory.Proposition_2_10_7_part2 {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory C M₂] [NonzeroModuleCategory M₂] (h : ∀ (F : ModuleFunctor C M₁ M₂), ModuleFunctorIsExact F) : ExactModuleCategory C M₁

Proposition 2.10.7 (EGNO), part 2: A module category M₁ over C is exact whenever every module functor from M₁ to any nonzero module category M₂ is exact.

@[reducible, inline]

abbrev CategoryTheory.Proposition_2_10_7 {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [LeftModuleCategory C M] (h : InternalHomExactInSecondVar C M) : ExactModuleCategory C M

Proposition 2.10.7 (EGNO): Convenient alias bundling the first criterion for a module category to be exact, namely exactness of the internal Hom in its second argument.