This book contains 376 definitions, 88 theorems, 110 propositions, 126 lemmas, 69 corollaries, 189 examples, 63 constructions, 74 remarks, 10 conventions, 4 criteria and 5 other statements.
209 of its 1,114 statements have been checked against Lean; 55 of those are formalized somewhere.
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
70 |
15 |
16 |
54 |
49 |
106 |
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
5 |
9 |
7 |
13 |
1 |
33 |
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
4 |
7 |
4 |
5 |
5 |
15 |
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
22 |
10 |
14 |
26 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
23 |
10 |
16 |
18 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
28 |
5 |
6 |
23 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
6 |
3 |
5 |
11 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
3 |
6 |
3 |
7 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
9 |
5 |
10 |
4 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
2 |
3 |
10 |
6 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
5 |
6 |
2 |
11 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
8 |
13 |
9 |
13 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
11 |
5 |
4 |
14 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
10 |
12 |
11 |
17 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
— |
13 |
4 |
13 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
23 |
2 |
5 |
12 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
14 |
9 |
11 |
16 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
21 |
5 |
4 |
19 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
22 |
14 |
7 |
8 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
26 |
18 |
17 |
21 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
14 |
5 |
11 |
8 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
18 |
12 |
11 |
12 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
27 |
5 |
3 |
12 |
not checked |
|
| FC11 — Peters–Sterk, Symmetric and Quadratic Forms (June 2024) |
5 |
6 |
5 |
2 |
not checked |
|
What the book contains
| Definitions |
376 |
| Theorems |
88 |
| Propositions |
110 |
| Lemmas |
126 |
| Corollaries |
69 |
| Examples |
189 |
| Constructions |
63 |
| Remarks |
74 |
| Conventions |
10 |
| Criteria |
4 |
| Other statements |
5 |
| Total |
1,114 |
Where its statements stand in Lean
| not formalized |
154 |
74% |
A documented search found no Lean statement of it anywhere. |
| in lean-categories |
40 |
19% |
This repository states and proves it. |
| in Mathlib |
10 |
5% |
Mathlib states and proves it. |
| in another Lean project |
5 |
2% |
Some other Lean development has it; using it means porting that code. |
| checked in total |
209 |
|
|
How this book was read
Frozen source: /home/dzack/Zotero/storage/ANG3AN65/[Peters 2024] Symmetric and Quadratic Forms, with Applications to Coding Theory, Algebraic Geometry and Topology.md.
This catalogue excludes exercises, proofs, bibliography/history prose, and purely expository recaps. Plural source example headings are represented by their first actual example and split into later reusable member examples. Source locators refer to the frozen Markdown extraction; a small number of OCR-lost display clauses were restored against the official June-2024 PDF without changing those anchors.