finitePresentation — Mathlib

English

If pres is a presentation with finite G and finite R, then M is finitely presented.

Русский

Если pres — презентация с конечными G и R, тогда M имеет конечно презентацию.

LaTeX

$$$[Finite pres.G] \\land [Finite pres.R] \\Rightarrow Module.FinitePresentation A M$$$

Lean4

theorem finitePresentation [Finite pres.G] [Finite pres.R] : Module.FinitePresentation A M :=
  Module.finitePresentation_of_surjective _ pres.surjective_π
    (by
      rw [pres.ker_π]
      exact Submodule.fg_span (Set.finite_range _))

Похожие утверждения