finitePresentation_of_isFinite — Mathlib

English

If σ and ι are finite, then the quotient is a finitely presented algebra; equivalently, the base algebra is finite-presented.

Русский

Если множества σ и ι конечны, то квотирование задаёт конечную презентацию.

LaTeX

$$$\\big[\\text{Finite }σ\\big]\\;\\big[\\text{Finite }ι\\big] \\Rightarrow FinitePresentation R S$$

Lean4

theorem finitePresentation_of_isFinite [Finite σ] [Finite ι] (P : Presentation R S ι σ) : FinitePresentation R S :=
  FinitePresentation.equiv (P.quotientEquiv.restrictScalars R)

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