mathlib3 documentation


The category of left R-modules is abelian. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Additionally, two linear maps are exact in the categorical sense iff range f = ker g.

@[protected, instance]
noncomputable def Module.abelian {R : Type u} [ring R] :

The category of R-modules is abelian.

theorem Module.exact_iff {R : Type u} [ring R] {M N : Module R} (f : M N) {O : Module R} (g : N O) :