YM
YM modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
YM.Dobrushin |
2 | 2 | 4 | 70 | — |
YM.Kernel |
0 | 0 | 4 | 43 | — |
YM.OS |
2 | 1 | 7 | 67 | — |
YM modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
YM.Dobrushin |
2 | 2 | 4 | 70 | — |
YM.Kernel |
0 | 0 | 4 | 43 | — |
YM.OS |
2 | 1 | 7 | 67 | — |