free_quotient — Mathlib

English

An unwrapped version: Polynomial.Monic.free_quotient states that the quotient by the ideal generated by a monic polynomial g is a free module over R.

Русский

Необертая версия: Polynomial.Monic.free_quotient утверждает, что quotient по идеалу, генерируемому моническим полиномом g, является свободным модулем над R.

LaTeX

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

Lean4

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

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