instFiniteIOverXQuasicoherentDataOfIsFinitePresentationRelationsPresentation

English

M is finite type; the associated data is finite.

Русский

M — конечного типа; соответствующие данные конечны.

LaTeX

$$$M\text{ is finite type}$$$

Lean4

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

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