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) ( Finset.univ fun i => Ideal.smithCoeffs b (Ideal.span {f}) (_ : ¬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.

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) :

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].