instPolynomial — Mathlib

English

If R is a finite type over itself, then the polynomial ring R[X] is also of finite type over R.

Русский

Если R само является конечной по типу над R, то R[X] тоже конечна по типу над R.

LaTeX

$$$[FiniteType R R] \\Rightarrow [FiniteType R (Polynomial R)]$$$

Lean4

instance [FiniteType R S] : FiniteType R S[X] :=
  by
  refine .trans ‹_› ⟨{ Polynomial.X }, ?_⟩
  rw [Finset.coe_singleton]
  exact Polynomial.adjoin_X

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