 Finitely presented module

A module is finitely presented if it has finitely many generators and finitely many defining relations, equivalently an exact sequence of the displayed form with m and n finite. Over a commutative ring a relation matrix records the presentation, and its minors define the Fitting ideals.

// Target: knot-theory.bigb