DSpace Zespół:
http://hdl.handle.net/11320/3332
2023-12-01T02:36:25ZAntiderivatives and Integration
http://hdl.handle.net/11320/15444
Tytuł: Antiderivatives and Integration
Autorzy: Endou, Noboru
Abstrakt: In this paper, we introduce indefinite integrals [8] (antiderivatives) and proof integration by substitution in the Mizar system [2], [3]. In our previous article [15], we have introduced an indefinite-like integral, but it is inadequate because it must be an integral over the whole set of real numbers and in some sense it causes some duplication in the Mizar Mathematical Library [13]. For this reason, to define the antiderivative for a function, we use the derivative of an arbitrary interval as defined recently in [7]. Furthermore, antiderivatives are also used to modify the integration by substitution and integration by parts. In the first section, we summarize the basic theorems on continuity and derivativity (for interesting survey of formalizations of real analysis in another proof-assistants like ACL2 [12], Isabelle/HOL [11], Coq [4], see [5]). In the second section, we generalize some theorems that were noticed during the formalization process. In the last section, we define the antiderivatives and formalize the integration by substitution and the integration by parts. We referred to [1] and [6] in our development.2023-01-01T00:00:00ZNormal Extensions
http://hdl.handle.net/11320/15443
Tytuł: Normal Extensions
Autorzy: Schwarzweller, Christoph
Abstrakt: In this article we continue the formalization of field theory in Mizar [1], [2], [4], [3]. We introduce normal extensions: an (algebraic) extension E of F is normal if every polynomial of F that has a root in E already splits in E. We proved characterizations (for finite extensions) by minimal polynomials [7], splitting fields, and fixing monomorphisms [6], [5]. This required extending results from [11] and [12], in particular that F[T] = {p(a1, . . . an) | p ∈ F[X], ai ∈ T} and F(T) = F[T] for finite algebraic T ⊆ E. We also provided the counterexample that Q(∛2) is not normal over Q (compare [13]).2023-01-01T00:00:00ZInternal Direct Products and the Universal Property of Direct Product Groups
http://hdl.handle.net/11320/15427
Tytuł: Internal Direct Products and the Universal Property of Direct Product Groups
Autorzy: Nelson, Alexander M.
Abstrakt: This is a “quality of life” article concerning product groups, using the Mizar system [2], [4]. Like a Sonata, this article consists of three movements. The first act, the slowest of the three, builds the infrastructure necessary for the rest of the article. We prove group homomorphisms map arbitrary finite products to arbitrary finite products, introduce a notion of “group yielding” families, as well as families of homomorphisms. We close the first act with defining the inclusion morphism of a subgroup into its parent group, and the projection morphism of a product group onto one of its factors. The second act introduces the universal property of products and its consequences as found in, e.g., Kurosh [7]. Specifically, for the product of an arbitrary family of groups, we prove the center of a product group is the product of centers. More exciting, we prove for a product of a finite family groups, the commutator subgroup of the product is the product of commutator subgroups, but this is
because in general: the direct sum of commutator subgroups is the subgroup of the commutator subgroup of the product group, and the commutator subgroup
of the product is a subgroup of the product of derived subgroups. We conclude this act by proving a few theorems concerning the image and kernel of morphisms between product groups, as found in Hungerford [5], as well as quotients of product groups. The third act introduces the notion of an internal direct product. Isaacs [6]
points out (paraphrasing with Mizar terminology) that the internal direct product is a predicate but the external direct product is a [Mizar] functor. To our delight, we find the bulk of the “recognition theorem” (as stated by Dummit and Foote [3], Aschbacher [1], and Robinson [11]) are already formalized in the heroic work of Nakasho, Okazaki, Yamazaki, and Shimada [9], [8]. We generalize the notion of an internal product to a set of subgroups, proving it is equivalent to the internal product of a family of subgroups [10].2023-01-01T00:00:00ZElementary Number Theory Problems. Part VIII
http://hdl.handle.net/11320/15424
Tytuł: Elementary Number Theory Problems. Part VIII
Autorzy: Korniłowicz, Artur
Abstrakt: In this paper problems 25, 86, 88, 105, 111, 137–142, and 184–185 from [12] are formalized, using the Mizar formalism [3], [1], [4]. This is a continuation of the work from [5], [6], and [2] as suggested in [8]. The auto matization of selected lemmas from [11] proven in this paper as proposed in [9] could be an interesting future work.2023-01-01T00:00:00Z