finrank_quotient_span_eq_natDegree'

English

Over a ring R with StrongRankCondition, for a monic f, the finrank of the quotient R[X]/(f) equals natDegree f.

Русский

Над кольцом R с условием StrongRankCondition для моноичного f, размерность quotient R[X]/(f) равна natDegree f.

LaTeX

$$$\\operatorname{Module.finrank} R \\bigl(R[X] \\Big/ \\langle f \\rangle\\bigr) = f.natDegree$$$

Lean4

/-- See `finrank_quotient_span_eq_natDegree` for a more general version over a field.
-/
theorem _root_.finrank_quotient_span_eq_natDegree' [StrongRankCondition R] (hf : f.Monic) :
    Module.finrank R (R[X] ⧸ Ideal.span { f }) = f.natDegree :=
  (AdjoinRoot.isAdjoinRootMonic _ hf).finrank

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