|
Mizar Mathematical Library
(version 5.94.1493) includes
1498 articles
written by
278 authors and
73460 theorems,
14291 definitions,
912 schemes,
19054 registrations,
10439 symbols.
(more statistics, other versions)
New:
monograph: TG Set Theory
authors by # of important facts
environment explanation
decode
-
Universal Property of Semidirect Products (Bourbaki~\cite[III \S2.10]{bourbaki2013general} Proposition 27) (submitted May 27, 2025)
formalized by
Alexander M. Nelson
-
Aschbacher~\cite{aschbacher2000finite}, Theorem 10.2 (submitted May 27, 2025)
formalized by
Alexander M. Nelson
-
Bourbaki~\cite[I \S6.1]{BourbakiAlgI}, Corollary to Proposition 4 (submitted May 27, 2025)
formalized by
Alexander M. Nelson
-
Universal Property of Quotient Groups (submitted May 27, 2025)
formalized by
Alexander M. Nelson
-
Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.4) (submitted May 27, 2025)
formalized by
Alexander M. Nelson
-
Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.3) (submitted May 27, 2025)
formalized by
Alexander M. Nelson
-
Aschbacher~\cite{aschbacher2000finite}, Theorem (10.1.3) (submitted May 27, 2025)
formalized by
Alexander M. Nelson
-
Conway Normal Form: (submitted April 10, 2025)
formalized by
Karol Pak
-
Now we apply the polynomial transformation 'F' to f_0. (submitted November 17, 2024)
formalized by
Yasushige Watase
-
Ring Extension version of REALALG3:16. (submitted November 17, 2024)
formalized by
Yasushige Watase
-
Ring Extended version of FIELD_13:13. (submitted November 17, 2024)
formalized by
Yasushige Watase
-
The following theorem corresponds to the equation (2) in \cite{HURWITZ:1893}. (submitted November 17, 2024)
formalized by
Yasushige Watase
-
Generalization of ZMATRLIN:42 ::: TODO (submitted November 17, 2024)
formalized by
Yasushige Watase
-
PROP 1.1.1 a) SGA4 (submitted November 8, 2024)
formalized by
Roland Coghetto
-
PROP 1.1.1 a) SGA4 (submitted November 8, 2024)
formalized by
Roland Coghetto
-
Conway Ch.1 Th.9 (submitted December 12, 2023)
formalized by
Karol Pak
-
Associativity of Multiplication for Surreal Numbers, Conway Ch.1 Th.7(iii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Distributivity of Multiplication Over Addition for Surreal Numbers, Conway Ch.1 Th.7(v) (submitted December 12, 2023)
formalized by
Karol Pak
-
Conway Ch.1 Th.7(in) (submitted December 12, 2023)
formalized by
Karol Pak
-
Multiplicative Identity for Surreal Number, Conway Ch.1 Th.7(ii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Conway Ch.1 Th.7(i) (submitted December 12, 2023)
formalized by
Karol Pak
-
Conway Ch.1 Th.8(iii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Conway Ch.1 Th.8(i) (submitted December 12, 2023)
formalized by
Karol Pak
-
Conway Ch.1 Th.4(i) (submitted December 12, 2023)
formalized by
Karol Pak
-
Property of The Aditive Inverse for Surreal Number, Conway Ch.1 Th.4(iii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Additive Identity for Surreal Number, Conway Ch.1 Th.3(i) (submitted December 12, 2023)
formalized by
Karol Pak
-
Associativity of Addition for Surreal Number, Conway Ch.1 Th.3(iii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Transitive Law of Addition for Surreal Number, Conway Ch.1 Th.5 (submitted December 12, 2023)
formalized by
Karol Pak
-
Commutativity of Addition for Surreal Number, Conway Ch.1 Th.3 (ii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Conway Ch.1 Th.4(ii) (submitted December 12, 2023)
formalized by
Karol Pak
-
The Simplicity Theorem for Surreal Numbers (submitted December 12, 2023)
formalized by
Karol Pak
-
Conway Ch.1 Th.2(i) (submitted December 12, 2023)
formalized by
Karol Pak
-
Preorder of Surreal Numbers - Total, Conway Ch.1 Th.2(ii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Preorder of Surreal Numbers - Transitivity, Conway Ch.1 Th.1 (submitted December 12, 2023)
formalized by
Karol Pak
-
Preorder of Surreal Numbers - Reflexivity, Conway Ch.1 Th.0(iii) (submitted December 12, 2023)
formalized by
Karol Pak
-
Relation with Polynomial Rings (submitted November 21, 2023)
formalized by
Yasushige Watase
-
Apply Embedding Principle to Rings. (submitted November 21, 2023)
formalized by
Yasushige Watase
-
Degree of directed regularity is unique. (submitted June 30, 2023)
formalized by
Sebastian Koch
-
Degree of regularity is unique. (submitted June 30, 2023)
formalized by
Sebastian Koch
-
Translation Bags 1 notation to NAT. (submitted March 31, 2023)
formalized by
Yasushige Watase
-
Prime Representing Polynomial with 10 Variables (submitted December 27, 2022)
formalized by
Karol Pak
-
Diophantine Representation of Prime Numbers with 8 Explicite Unknowns (submitted December 27, 2022)
formalized by
Karol Pak
-
Diophantine Representation of Solutions to Pell's Equation (submitted December 27, 2022)
formalized by
Karol Pak
MML links:
Latest 30 articles (the query:
list of article ordered by historical order reversed select 0-29)
-
group_24:
Semidirect Products of Groups
by
Alexander M. Nelson
(submitted May 27, 2025)
117 theorems,
9 definitions,
no schemes,
17 registrations,
authors:Alexander M Nelson,
abstract,
semantically linked,
FM
,
full article,
gab.
-
polnot_2:
Extensions of Languages in Polish Notation
by
Taneli Huuskonen
(submitted May 23, 2025)
21 theorems,
25 definitions,
no schemes,
18 registrations,
authors:Taneli Huuskonen,
abstract,
semantically linked,
FM
,
full article,
gab.
-
newton06:
Application of Complex Classes to Number Theory
by
Rafal Ziobro
(submitted May 11, 2025)
83 theorems,
no definitions,
no schemes,
99 registrations,
authors:Rafal Ziobro,
abstract,
semantically linked,
FM
,
full article,
gab.
-
gr_free0:
Free Product of Groups
by
Sebastian Koch
(submitted April 27, 2025)
73 theorems,
13 definitions,
no schemes,
23 registrations,
authors:Sebastian Koch,
abstract,
semantically linked,
FM
,
full article,
gab.
-
surrealc:
Conway's Normal Form in the Mizar System
by
Karol Pak
(submitted April 10, 2025)
106 theorems,
23 definitions,
1 scheme,
24 registrations,
authors:Karol Pak,
abstract,
semantically linked,
FM
,
full article,
gab.
-
surrealn:
Surreal Dyadic and Real Numbers: A Formal Construction
by
Karol Pak
(submitted April 10, 2025)
80 theorems,
12 definitions,
no schemes,
31 registrations,
authors:Karol Pak,
abstract,
semantically linked,
FM
,
full article,
gab.
-
surreals:
Surreal Numbers: A Study of Square Roots
by
Karol Pak
(submitted April 10, 2025)
32 theorems,
9 definitions,
no schemes,
9 registrations,
authors:Karol Pak,
abstract,
semantically linked,
FM
,
full article,
gab.
-
field_16:
Finite Fields
by
Christoph Schwarzweller
(submitted December 27, 2024)
73 theorems,
8 definitions,
1 scheme,
50 registrations,
authors:Christoph Schwarzweller,
abstract,
semantically linked,
FM
,
full article,
gab.
-
relset_3:
Some Number Relations
by
Sebastian Koch
(submitted December 27, 2024)
78 theorems,
4 definitions,
no schemes,
17 registrations,
authors:Sebastian Koch,
abstract,
semantically linked,
FM
,
full article,
gab.
-
latwal_2:
Formalization of Trellises and Tolerance Relations
by
Adam Grabowski,
Franciszek Turowski
(submitted December 27, 2024)
39 theorems,
16 definitions,
no schemes,
25 registrations,
authors:Adam Grabowski. Franciszek Turowski,
abstract,
semantically linked,
FM
,
full article,
gab.
-
ndiff13:
Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces
by
Kazuhisa Nakasho,
Yasunari Shidama
(submitted December 24, 2024)
66 theorems,
3 definitions,
no schemes,
no registrations,
authors:Kazuhisa Nakasho. Yasunari Shidama,
abstract,
semantically linked,
FM
,
full article,
gab.
-
newton07:
Pascal's Triangle and Lucas's Theorem
by
Rafal Ziobro
(submitted December 24, 2024)
102 theorems,
3 definitions,
no schemes,
35 registrations,
authors:Rafal Ziobro,
abstract,
semantically linked,
FM
,
full article,
gab.
-
vectsp13:
Some Standard Examples of Vector Spaces
by
Christoph Schwarzweller,
Agnieszka Rowinska-Schwarzweller
(submitted December 24, 2024)
41 theorems,
24 definitions,
no schemes,
34 registrations,
authors:Agnieszka Schwarzweller. Christoph Schwarzweller,
abstract,
semantically linked,
FM
,
full article,
gab.
-
proofs_1:
Fundamentals of Finitary Proofs
by
Taneli Huuskonen
(submitted December 24, 2024)
25 theorems,
36 definitions,
3 schemes,
38 registrations,
authors:Taneli Huuskonen,
abstract,
semantically linked,
FM
,
full article,
gab.
-
number16:
Elementary Number Theory Problems. Part XVI
by
Karol Pak
(submitted December 14, 2024)
40 theorems,
no definitions,
no schemes,
no registrations,
authors:Karol Pak,
abstract,
semantically linked,
FM
,
full article,
gab.
-
pdlax:
Classical Isoperimetric Theorem
by
Kazuhisa Nakasho,
Yasunari Shidama
(submitted December 14, 2024)
17 theorems,
no definitions,
no schemes,
no registrations,
authors:Kazuhisa Nakasho. Yasunari Shidama,
abstract,
semantically linked,
FM
,
full article,
gab.
-
glpacy00:
About Path and Cycle Graphs
by
Sebastian Koch
(submitted December 9, 2024)
47 theorems,
10 definitions,
no schemes,
98 registrations,
authors:Sebastian Koch,
abstract,
semantically linked,
FM
,
full article,
gab.
-
ndiff12:
Differentiability Properties of Lipschitzian Bilinear Operators in Real Normed Spaces
by
Kazuhisa Nakasho,
Yasunari Shidama
(submitted December 9, 2024)
21 theorems,
no definitions,
no schemes,
no registrations,
authors:Kazuhisa Nakasho. Yasunari Shidama,
abstract,
semantically linked,
FM
,
full article,
gab.
-
measur14:
Universality of Measure Space
by
Noboru Endou,
Yasunari Shidama
(submitted December 9, 2024)
55 theorems,
12 definitions,
no schemes,
1 registration,
authors:Noboru Endou. Yasunari Shidama,
abstract,
semantically linked,
FM
,
full article,
gab.
-
ascoli2:
Ascoli-Arzela's Theorem (Metric Space Version)
by
Keiichi Miyajima,
Hiroshi Yamazaki
(submitted November 28, 2024)
21 theorems,
6 definitions,
no schemes,
4 registrations,
authors:Keiichi Miyajima. Hiroshi Yamazaki,
abstract,
semantically linked,
FM
,
full article,
gab.
-
dualsp06:
Formalization of Orthogonal Complements of Normed Spaces
by
Hiroyuki Okazaki
(submitted November 28, 2024)
25 theorems,
6 definitions,
no schemes,
no registrations,
authors:Hiroyuki Okazaki,
abstract,
semantically linked,
FM
,
full article,
gab.
-
e_trans2:
Formal Proof of Transcendence of the Number $e$. Part II
by
Yasushige Watase
(submitted November 17, 2024)
42 theorems,
9 definitions,
no schemes,
2 registrations,
authors:Yasushige Watase,
abstract,
semantically linked,
FM
,
full article,
gab.
-
e_trans1:
Formal Proof of Transcendence of the Number $e$. Part I
by
Yasushige Watase
(submitted November 17, 2024)
38 theorems,
10 definitions,
no schemes,
8 registrations,
authors:Yasushige Watase,
abstract,
semantically linked,
FM
,
full article,
gab.
-
number15:
Elementary Number Theory Problems. Part XV -- Diophantine Equations
by
Karol Pkak,
Artur Kornilowicz
(submitted November 8, 2024)
90 theorems,
16 definitions,
1 scheme,
74 registrations,
authors:Artur Kornilowicz. Karol Pkak,
abstract,
semantically linked,
FM
,
full article,
gab.
-
classes5:
U-Small and U-Locally Small Categories
by
Roland Coghetto
(submitted November 8, 2024)
111 theorems,
37 definitions,
no schemes,
27 registrations,
authors:Roland Coghetto,
abstract,
semantically linked,
FM
,
full article,
gab.
-
surreali:
Inverse Element for Surreal Number
by
Karol Pak
(submitted October 22, 2024)
45 theorems,
15 definitions,
no schemes,
8 registrations,
authors:Karol Pak,
abstract,
semantically linked,
FM
,
full article,
gab.
-
number14:
Elementary Number Theory Problems. Part XIV -- Diophantine Equations
by
Artur Kornilowicz
(submitted October 22, 2024)
112 theorems,
19 definitions,
no schemes,
30 registrations,
authors:Artur Kornilowicz,
abstract,
semantically linked,
FM
,
full article,
gab.
-
field_15:
Separable Polynomials and Separable Extensions
by
Christoph Schwarzweller
(submitted June 18, 2024)
94 theorems,
6 definitions,
no schemes,
37 registrations,
authors:Christoph Schwarzweller,
abstract,
semantically linked,
FM
,
full article,
gab.
-
mesfun17:
Integral of Continuous Three Variable Functions
by
Noboru Endou,
Yasunari Shidama
(submitted June 18, 2024)
69 theorems,
no definitions,
no schemes,
no registrations,
authors:Noboru Endou. Yasunari Shidama,
abstract,
semantically linked,
FM
,
full article,
gab.
-
number13:
Elementary Number Theory Problems. Part XIII
by
Artur Kornilowicz,
Rafal Ziobro
(submitted June 18, 2024)
54 theorems,
5 definitions,
no schemes,
13 registrations,
authors:Artur Kornilowicz. Rafal Ziobro,
abstract,
semantically linked,
FM
,
full article,
gab.
Full list in reversed historical order
(start querying)
and lexical order
of MML Id,
titles,
authors.
- version 5.94.1493
- version 5.68.1412
[differences]
- version 5.57.1355
[differences]
- version 5.45.1305
[differences]
- version 5.33.1254
[differences]
- version 5.25.1220
[differences]
[Compare two versions]
|
|