instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs

English

In a finite-dimensional setting over F, the quotient by a single element relates to the natDegree of its norm.

Русский

В конечном размерном случае фактор по одному элементу связан с natDegree нормы элемента.

LaTeX

$$finrank (S/I) = (Algebra.norm F[X] f).natDegree$$

Lean4

instance (b : Basis ι F[X] S) {I : Ideal S} (hI : I ≠ ⊥) (i : ι) :
    FiniteDimensional F (F[X] ⧸ span ({I.smithCoeffs b hI i} : Set F[X])) :=
  PowerBasis.finite <| AdjoinRoot.powerBasis <| I.smithCoeffs_ne_zero b hI i

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