OAI/Combinatorics/RamseyFive/Geometry/BasePublicFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.ScoreGeometry.BaseTape line 15
2. def OAI.SharpRamseyFive.ScoreGeometry.baseRowMeasure line 18
3. def OAI.SharpRamseyFive.ScoreGeometry.baseTapeMeasure line 22
4. instance OAI.SharpRamseyFive.ScoreGeometry.(instance at line 26) line 26
5. instance OAI.SharpRamseyFive.ScoreGeometry.(instance at line 31) line 31
6. lemma OAI.SharpRamseyFive.ScoreGeometry.baseTape_marginal line 37
7. def OAI.SharpRamseyFive.ScoreGeometry.baseMessageDecoded line 47