English
For a nonzero f in an S-module over a polynomial ring, the finite rank of S/⟨f⟩ equals the natDegree of the norm of f.
Русский
Для не нулевого f в модуле над F[X] фактор-модуль S/⟨f⟩ имеет размерность, равную natDegree нормы f.
LaTeX
$$Module.finrank_F(S/⟨f⟩) = (Algebra.norm (Polynomial F) f).natDegree$$
Lean4
/-- 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]`. -/
theorem finrank_quotient_span_eq_natDegree_norm [Algebra F S] [IsScalarTower F F[X] S] (b : Basis ι F[X] S) {f : S}
(hf : f ≠ 0) : Module.finrank F (S ⧸ span ({ f } : Set S)) = (Algebra.norm F[X] f).natDegree :=
by
haveI := Fintype.ofFinite ι
have h := span_singleton_eq_bot.not.2 hf
rw [natDegree_eq_of_degree_eq (degree_eq_degree_of_associated <| associated_norm_prod_smith b hf)]
rw [natDegree_prod _ _ fun i _ => smithCoeffs_ne_zero b _ h i, finrank_quotient_eq_sum F h b]
congr with i
exact (AdjoinRoot.powerBasis <| smithCoeffs_ne_zero b _ h i).finrank
