Currently displaying 1 – 11 of 11

Showing per page

Order by Relevance | Title | Year of publication

Proth Numbers

Christoph Schwarzweller — 2014

Formalized Mathematics

In this article we introduce Proth numbers and prove two theorems on such numbers being prime [3]. We also give revised versions of Pocklington’s theorem and of the Legendre symbol. Finally, we prove Pepin’s theorem and that the fifth Fermat number is not prime.

Introduction to Rational Functions

Christoph Schwarzweller — 2012

Formalized Mathematics

In this article we formalize rational functions as pairs of polynomials and define some basic notions including the degree and evaluation of rational functions [8]. The main goal of the article is to provide properties of rational functions necessary to prove a theorem on the stability of networks

Modular Integer Arithmetic

Christoph Schwarzweller — 2008

Formalized Mathematics

In this article we show the correctness of integer arithmetic based on Chinese Remainder theorem as described e.g. in [11]: Integers are transformed to finite sequences of modular integers, on which the arithmetic operations are performed. Retransformation of the results to the integers is then accomplished by means of the Chinese Remainder theorem. The method presented is a typical example for computing in homomorphic images.

On Roots of Polynomials and Algebraically Closed Fields

Christoph Schwarzweller — 2017

Formalized Mathematics

In this article we further extend the algebraic theory of polynomial rings in Mizar [1, 2, 3]. We deal with roots and multiple roots of polynomials and show that both the real numbers and finite domains are not algebraically closed [5, 7]. We also prove the identity theorem for polynomials and that the number of multiple roots is bounded by the polynomial’s degree [4, 6].

Ordered Rings and Fields

Christoph Schwarzweller — 2017

Formalized Mathematics

We introduce ordered rings and fields following Artin-Schreier’s approach using positive cones. We show that such orderings coincide with total order relations and give examples of ordered (and non ordered) rings and fields. In particular we show that polynomial rings can be ordered in (at least) two different ways [8, 5, 4, 9]. This is the continuation of the development of algebraic hierarchy in Mizar [2, 3].

The First Isomorphism Theorem and Other Properties of Rings

Artur KorniłowiczChristoph Schwarzweller — 2014

Formalized Mathematics

Different properties of rings and fields are discussed [12], [41] and [17]. We introduce ring homomorphisms, their kernels and images, and prove the First Isomorphism Theorem, namely that for a homomorphism f : R → S we have R/ker(f) ≅ Im(f). Then we define prime and irreducible elements and show that every principal ideal domain is factorial. Finally we show that polynomial rings over fields are Euclidean and hence also factorial

Characteristic of Rings. Prime Fields

Christoph SchwarzwellerArtur Korniłowicz — 2015

Formalized Mathematics

The notion of the characteristic of rings and its basic properties are formalized [14], [39], [20]. Classification of prime fields in terms of isomorphisms with appropriate fields (ℚ or ℤ/p) are presented. To facilitate reasonings within the field of rational numbers, values of numerators and denominators of basic operations over rationals are computed.

Some Algebraic Properties of Polynomial Rings

Christoph SchwarzwellerArtur Korniłowicz — 2016

Formalized Mathematics

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.

A Test for the Stability of Networks

Agnieszka Rowinska-SchwarzwellerChristoph Schwarzweller — 2013

Formalized Mathematics

A complex polynomial is called a Hurwitz polynomial, if all its roots have a real part smaller than zero. This kind of polynomial plays an all-dominant role in stability checks of electrical (analog or digital) networks. In this article we prove that a polynomial p can be shown to be Hurwitz by checking whether the rational function e(p)/o(p) can be realized as a reactance of one port, that is as an electrical impedance or admittance consisting of inductors and capacitors. Here e(p) and o(p) denote...

Schur's Theorem on the Stability of Networks

Christoph SchwarzwellerAgnieszka Rowińska-Schwarzweller — 2006

Formalized Mathematics

A complex polynomial is called a Hurwitz polynomial if all its roots have a real part smaller than zero. This kind of polynomial plays an all-dominant role in stability checks of electrical networks.In this article we prove Schur's criterion [17] that allows to decide whether a polynomial p(x) is Hurwitz without explicitly computing its roots: Schur's recursive algorithm successively constructs polynomials pi(x) of lesser degree by division with x - c, ℜ {c} < 0, such that pi(x) is Hurwitz if...

Page 1

Download Results (CSV)