instMvPolynomialOfFinite — Mathlib

English

If f is surjective and ker f is FG, then f is finitely presented.

Русский

Если f сюръективен и ядро FG, то f конечнопредставим.

LaTeX

$$$\\text{Surjective}(f) \\land (\\ker f) FG \\Rightarrow f.FinitePresentation$$$

Lean4

instance {ι : Type*} [Finite ι] [FiniteType R S] : FiniteType R (MvPolynomial ι S) := by
  classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact MvPolynomial.adjoin_range_X

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