finitePresentation — Mathlib

English

There is a finite presentation of AdjoinRoot f over S given by a quotient of a finitely generated submodule (or ideal).

Русский

Существует конечная презентация AdjoinRoot f над S через факторизацию по порождающему подмодулю/идеалу.

LaTeX

$$$FinitePresentation S (AdjoinRoot f)$$$

Lean4

instance finitePresentation [CommRing S] [Algebra S R] [FinitePresentation S R] : FinitePresentation S (AdjoinRoot f) :=
  .quotient (Submodule.fg_span_singleton f)

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