instFinitePresentationModelOfHasCoeffsOfFinite

English

If ι and σ are finite, then the ModelOfHasCoeffs is a finitely presented algebra over R0.

Русский

Если ι и σ конечны, то ModelOfHasCoeffs является финитомно презентабельной алгеброй над R0.

LaTeX

$$$\\text{Finite } (ι) \\land \\text{Finite } (\\sigma) \\Rightarrow \\text{Algebra.FinitePresentation } R_0 (P.\\mathrm{ModelOfHasCoeffs} R_0)$$$

Lean4

instance [Finite ι] [Finite σ] : Algebra.FinitePresentation R₀ (P.ModelOfHasCoeffs R₀) := by
  classical
  cases nonempty_fintype σ
  exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩

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