# Norms on free modules over principal ideal domains #

theorem associated_norm_prod_smith {R : Type u_1} {S : Type u_2} {ι : Type u_3} [] [] [] [] [Algebra R S] [] (b : Basis ι R S) {f : S} (hf : f 0) :
Associated (() f) (i : ι, Ideal.smithCoeffs b (Ideal.span {f}) i)

For a nonzero element f in an algebra S over a principal ideal domain R that is finite and free as an R-module, the norm of f relative to R is associated to the product of the Smith coefficients of the ideal generated by f.

instance instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs {S : Type u_2} {ι : Type u_3} [] [] {F : Type u_4} [] [Algebra () S] [] (b : Basis ι () S) {I : } (hI : I ) (i : ι) :
Equations
• =
theorem finrank_quotient_span_eq_natDegree_norm {S : Type u_2} {ι : Type u_3} [] [] {F : Type u_4} [] [Algebra () S] [] [Algebra F S] [IsScalarTower F () S] (b : Basis ι () S) {f : S} (hf : f 0) :
FiniteDimensional.finrank F (S Ideal.span {f}) = (() f).natDegree

For a nonzero element f in a F[X]-module S, the dimension of $S/\langle f \rangle$ as an F-vector space is the degree of the norm of f relative to F[X].