finrank_quotient_span_eq_natDegree

English

The free structure on AdjoinRoot g is given by a basis of powers of the root when g is nonzero.

Русский

Свободная структура на AdjoinRoot g задается базисом степеней корня при g ≠ 0.

LaTeX

$$Polynomial.Monic.free_adjoinRoot hf$$

Lean4

/-- See `finrank_quotient_span_eq_natDegree'` for a version over a ring when `f` is monic.
-/
theorem _root_.finrank_quotient_span_eq_natDegree {f : K[X]} :
    Module.finrank K (K[X] ⧸ Ideal.span { f }) = f.natDegree :=
  by
  by_cases hf : f = 0
  · rw [hf, natDegree_zero, ((Submodule.quotEquivOfEqBot _ (by simp)).restrictScalars K).finrank_eq]
    exact finrank_of_not_finite Polynomial.not_finite
  rw [PowerBasis.finrank]
  exact AdjoinRoot.powerBasis_dim hf

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