instFiniteIOverXQuasicoherentDataOfIsFinitePresentationGeneratorsPresentation

English

The relations in the presentation over X are finite.

Русский

Отношения в презентации над X конечны.

LaTeX

$$$\text{Finite}\ (\mathrm{presentation}_{i}.\mathrm{relations}.I)$$$

Lean4

instance (i : M.quasicoherentDataOfIsFinitePresentation.I) :
    Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).generators.I :=
  have : _ ∧ Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).relations.I :=
    h.exists_quasicoherentData.choose_spec i
  this.1

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