mathlib3documentation

linear_algebra.free_module.norm

Norms on free modules over principal ideal domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem associated_norm_prod_smith {R : Type u_1} {S : Type u_2} {ι : Type u_3} [comm_ring R] [is_domain R] [comm_ring S] [is_domain S] [ S] [fintype ι] (b : R S) {f : S} (hf : f 0) :
associated ((algebra.norm R) f) (finset.univ.prod (λ (i : ι), (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.

@[protected, instance]
def has_quotient.quotient.finite_dimensional {S : Type u_2} {ι : Type u_3} [comm_ring S] [is_domain S] {F : Type u_4} [field F] [ S] [finite ι] (b : (polynomial F) S) {I : ideal S} (hI : I ) (i : ι) :
ideal.span hI i})
theorem finrank_quotient_span_eq_nat_degree_norm {S : Type u_2} {ι : Type u_3} [comm_ring S] [is_domain S] {F : Type u_4} [field F] [ S] [finite ι] [ S] [ S] (b : (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].