Characteristic polynomial/Definition/Field/Remark

In this definition, we use the determinant of a matrix, which we have only defined for matrices with entries in a field. The entries are now elements of the polynomial ring ${}K[X]$. But, since we can consider these elements also inside the field of rational functions ${}K(X)$, this is a useful definition. By definition, the determinant is an element in ${}K(X)$, but, because all entries of the matrix are polynomials, and because in the recursive definition of the determinant, only addition and multiplication is used, the characteristic polynomial is indeed a polynomial.