OAI/GroupTheory/SimpleAmenable/CentralCovers/PrimitiveCopies.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SimpleAmenable.InitialCoverSystem.initialConditionalline 20 - theorem
OAI.SimpleAmenable.InitialCoverSystem.initialConditional_inputline 24 - theorem
OAI.SimpleAmenable.InitialCoverSystem.initialConditional_projectionline 29 - theorem
OAI.SimpleAmenable.InitialCoverSystem.initialConditional_zeroline 37 - def
OAI.SimpleAmenable.InitialCoverSystem.initialAlphabetline 40 - theorem
OAI.SimpleAmenable.InitialCoverSystem.initialAlphabet_alignedline 44 - def
OAI.SimpleAmenable.InitialCoverSystem.translatedAlphabetline 67 - theorem
OAI.SimpleAmenable.InitialCoverSystem.translatedAlphabet_alignedline 72 - theorem
OAI.SimpleAmenable.InitialCoverSystem.initialAlphabet_orbit_independentline 77