Theorems · Theorem · commutative algebra

finrank_quotient_span_eq_natDegree_norm

∀ {S : Type u_2} {ι : Type u_3} [inst : CommRing S] [IsDomain S] {F : Type u_4} [inst_2 : Field F]
  [inst_3 : Algebra (Polynomial F) S] [Finite ι] [inst_5 : Algebra F S] [IsScalarTower F (Polynomial F) S]
  (b : Module.Basis ι (Polynomial F) S) {f : S},
  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].

Defined in

Mathlib.LinearAlgebra.FreeModule.Norm

Cited by

1 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainFieldAlgebraFiniteAlgebraIsScalarTower