Norms on free modules over principal ideal domains

theorem associated_norm_prod_smith {R : Type u_1} {S : Type u_2} {ι : Type u_3} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [CommRing S] [IsDomain S] [Algebra R S] [Fintype ι] (b : Basis ι R S) {f : S} (hf : f ≠ 0) : Associated ((Algebra.norm R) 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} [CommRing S] [IsDomain S] {F : Type u_4} [Field F] [Algebra (Polynomial F) S] [Finite ι] (b : Basis ι (Polynomial F) S) {I : Ideal S} (hI : I ≠ ⊥) (i : ι) : FiniteDimensional F (Polynomial F ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})

theorem finrank_quotient_span_eq_natDegree_norm {S : Type u_2} {ι : Type u_3} [CommRing S] [IsDomain S] {F : Type u_4} [Field F] [Algebra (Polynomial F) S] [Finite ι] [Algebra F S] [IsScalarTower F (Polynomial F) S] (b : Basis ι (Polynomial F) S) {f : S} (hf : f ≠ 0) : Module.finrank F (S ⧸ Ideal.span {f}) = ((Algebra.norm (Polynomial 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].