http://hdl.handle.net/11320/19588 Mon, 01 Jun 2026 19:15:35 GMT 2026-06-01T19:15:35Z http://hdl.handle.net/11320/19740 Tytuł: Elementary Number Theory Problems. Part XIX Autorzy: Pąk, Karol Abstrakt: In this paper, we present formal solutions to twelve problems selected from Wacław Sierpiński’s book 250 Problems in Elementary Number Theory. The selected problems are: 108, 112–114, 118–119, 127, 129, 130, and 132–134 formalized in the Mizar system. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19740 2025-01-01T00:00:00Z http://hdl.handle.net/11320/19739 Tytuł: Characterization of Finite Galois Extensions Autorzy: Schwarzweller, Christoph Abstrakt: In this article we prove the well-known characterization of finite Galois extensions: a finite extension E of F is a Galois extension of F iff E is both normal and separable iff E is the splitting field of a separable polynomial p ∈ F[X]. We also prove some applications of the characterization, so for example that F(a1, . . . , an) is a separable extension of F if and only if all the ai are separable, or that every finite separable extension of F is contained in a Galois extension of F. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19739 2025-01-01T00:00:00Z http://hdl.handle.net/11320/19738 Tytuł: Formalization of Separable Version of Banach–Alaoglu Theorem Autorzy: Okazaki, Hiroyuki; Mieno, Takehiko Abstrakt: In this article, we first formalize the weak sequential compactness in dual normed spaces; then we prove the separable version of Banach– Alaoglu theorem. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19738 2025-01-01T00:00:00Z http://hdl.handle.net/11320/19737 Tytuł: Elementary Number Theory Problems. Part XVIII Autorzy: Grabowski, Adam Abstrakt: In this paper another seven problems from Wacław Sierpiński’s book “250 Problems in Elementary Number Theory” are formalized, using the Mizar formalism, namely: 53, 61, 81, 90, 100, 156, and 167. Wed, 01 Jan 2025 00:00:00 GMT http://hdl.handle.net/11320/19737 2025-01-01T00:00:00Z