OAI/NumberTheory/Ostmann/Construction/CanonicalOccurrenceTransportDecodedData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.Construction.CanonicalOccurrenceTransport.DecodedDraw line 11
2. abbrev OAI.Ostmann.Construction.CanonicalOccurrenceTransport.DecodedDraw.history line 22
3. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.DecodedDraw.labels line 25
4. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.DecodedDraw.SameFrequencies line 28
5. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.DecodedDraw.normalizedRows_eq line 32
6. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.DecodedDraw.normalizedCode_eq line 38