English
An arbitrary choice of a finite presentation of a finitely presented algebra is made, selecting a particular Fin(n) and Fin(m) together with a presentation.
Русский
Произвольный выбор конечной презентации конечной презентации над данными кольцами, выбирая конкретные Fin(n) и Fin(m) вместе с презентацией.
LaTeX
$$$\\mathrm{ofFinitePresentation} \\,[\\text{FinitePresentation } R S] : \\mathrm{Presentation}\\; R\\; S\\; (\\mathrm{Fin} (\\mathrm{ofFinitePresentationVars } R S))\\; (\\mathrm{Fin} (\\mathrm{ofFinitePresentationRels } R S))$$$
Lean4
/-- An arbitrary choice of a finite presentation of a finitely presented algebra. -/
noncomputable def ofFinitePresentation [FinitePresentation R S] :
Presentation R S (Fin (ofFinitePresentationVars R S)) (Fin (ofFinitePresentationRels R S)) :=
(exists_presentation_fin R S).choose_spec.choose_spec.some
