This formalization also contains an abstract representation as coefficient functions with finite support and a type of power-products. If this type is ordered by a linear (term) ordering, various additional notions, such as leading power-product, leading coefficient etc., are introduced as well. Furthermore, a lot of generic properties of, and functions on, multivariate polynomials are formalized, including the substitution and evaluation homomorphisms, embeddings of polynomial rings into larger rings (i.e. with one additional indeterminate), homogenization and dehomogenization of polynomials, and the canonical isomorphism between R[X,Y] and R[X][Y].
- April 18, 2019
- Added material about polynomials whose power-products are represented themselves by polynomial mappings.
- January 23, 2018
- Added authors Haftmann, Lochbihler after incorporating
their formalization of multivariate polynomials based on Polynomial mappings.
Moved material from Bentkamp's entry "Deep Learning".
- October 28, 2016
- Added abstract representation of polynomials and authors Maletzky/Immler.
- September 17, 2010
- Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.