http://hdl.handle.net/11320/19588 2026-06-01T17:24:42Z 2026-06-01T17:24:42Z Pąk, Karol http://hdl.handle.net/11320/19740 2026-02-02T13:53:08Z 2025-01-01T00:00:00Z

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.

2025-01-01T00:00:00Z Schwarzweller, Christoph http://hdl.handle.net/11320/19739 2026-02-02T13:13:17Z 2025-01-01T00:00:00Z

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.

2025-01-01T00:00:00Z Okazaki, Hiroyuki Mieno, Takehiko http://hdl.handle.net/11320/19738 2026-02-02T12:56:04Z 2025-01-01T00:00:00Z

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.

2025-01-01T00:00:00Z Grabowski, Adam http://hdl.handle.net/11320/19737 2026-02-02T12:02:22Z 2025-01-01T00:00:00Z

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.

2025-01-01T00:00:00Z