http://hdl.handle.net/11320/17706 2026-03-08T04:37:37Z http://hdl.handle.net/11320/17809 Tytuł: Finite Fields Autorzy: Schwarzweller, Christoph Abstrakt: We continue the formalization of field theory in Mizar. Here we prove existence and uniqueness of finite fields by constructing the splitting field of the polynomial X (pⁿ) −X over the prime field of a field with characteristic p. We also define the Frobenius morphism and show that the automorphisms of a field with pⁿ elements are exactly the powers 0, . . . , n − 1 of the Frobenius morphism, that is the automorphism group is generated by the Frobenius morphism. 2024-01-01T00:00:00Z http://hdl.handle.net/11320/17806 Tytuł: Some Number Relations Autorzy: Koch, Sebastian Abstrakt: In this article some number relations are formalized in the Mizar system. 2024-01-01T00:00:00Z http://hdl.handle.net/11320/17802 Tytuł: Formalization of Trellises and Tolerance Relations Autorzy: Grabowski, Adam; Turowski, Franciszek Abstrakt: The main aim of this article is to construct two non-trivial examples of weakly associative lattices (also known as trellises). These are generalizations of lattices, not assuming associativity of the lattice operations. We show some connections between trellises and tolerance relations according to the paper of Chajda and Zelinka. 2024-01-01T00:00:00Z http://hdl.handle.net/11320/17801 Tytuł: Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces Autorzy: Nakasho, Kazuhisa; Shidama, Yasunari Abstrakt: This article extends the formalization of the theory of differentiation in real normed spaces in the Mizar system. The focus is on higher-order derivatives and the inverse function theorem. Additionally, we encode the differentiability of the inversion operator on invertible linear operators. 2024-01-01T00:00:00Z