finite_quotient — Mathlib

English

Polynomial.Monic.finite_quotient asserts that the quotient by the principal ideal generated by a monic g is a finite module over R.

Русский

Polynomial.Monic.finite_quotient утверждает, что фактор-кольцо по порожденному монитиком g идеалу — конечный модуль над R.

LaTeX

$$Module.Finite R (R[X] ⧸ Ideal.span { g }) holds when g is Monic$$

Lean4

/-- An unwrapped version of `AdjoinRoot.finite_of_monic` for better discoverability. -/
theorem _root_.Polynomial.Monic.finite_quotient (hg : g.Monic) : Module.Finite R (R[X] ⧸ Ideal.span { g }) :=
  hg.finite_adjoinRoot

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