instFinitePresentationQuotientOfFinite

English

If the presentation is finite, then the quotient has finite presentation.

Русский

Если презентация конечна, то квотент имеет конечную презентацию.

LaTeX

$$instance [Finite σ] [Finite ι] : FinitePresentation R P.Quotient := FinitePresentation.quotient P.fg_ker$$

Lean4

/-- If a presentation is finite, the corresponding quotient is
of finite presentation. -/
instance [Finite σ] [Finite ι] : FinitePresentation R P.Quotient :=
  FinitePresentation.quotient P.fg_ker

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