Some algebraic aspects of quadratic forms over fields of characteristic two.
In this article we extend the algebraic theory of polynomial rings, formalized in Mizar [1], based on [2], [3]. After introducing constant and monic polynomials we present the canonical embedding of R into R[X] and deal with both unit and irreducible elements. We also define polynomial GCDs and show that for fields F and irreducible polynomials p the field F[X]/ is isomorphic to the field of polynomials with degree smaller than the one of p.
Let () be the -ring of all (bounded) real-measurable functions on a -measurable space , let be the family of all such that is compact, and let be all that is compact for any . We introduce realcompact subrings of , we show that is a realcompact subring of , and also is a realcompact if and only if is a compact measurable space. For every nonzero real Riesz map , we prove that there is an element such that for every if is a compact measurable space. We confirm...