Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant (Q6572563)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant |
scientific article; zbMATH DE number 7881138
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant |
scientific article; zbMATH DE number 7881138 |
Statements
Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant (English)
0 references
15 July 2024
0 references
coq
0 references
projective geometry
0 references
finite models
0 references
spreads
0 references
packings
0 references
PG(3,2)
0 references
