Norm for (finite) ring extensions #
Suppose we have an
S with a finite basis. For each
s : S,
the determinant of the linear map given by multiplying by
s gives information
about the roots of the minimal polynomial of
Implementation notes #
Typically, the norm is defined specifically for finite field extensions. The current definition is as general as possible and the assumption that we have fields or that the extension is finite is added to the lemmas as needed.
Algebra.trace, which is defined similarly as the trace of
x is in the base field
K, then the norm is
x ^ [L : K].
L is not finite-dimensional over
norm = 1 = x ^ 0 = x ^ (finrank L K).)
pb : PowerBasis K S, then the norm of
(-1) ^ pb.dim * coeff (minpoly K pb.gen) 0.
pb : PowerBasis R S, then the norm of
((minpoly R pb.gen).aroots F).prod.
L/K a finite separable extension of fields and
E an algebraically closed extension
K, the norm (down to
K) of an element
L is equal to the product of the images
x over all the