OAI/GroupTheory/SimpleAmenable/CentralCovers/SmallSectorGeneration.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.SimpleAmenable.FiveSubalphabetline 16 - instance
OAI.SimpleAmenable.fiveSubalphabet_perfectline 18 - theorem
OAI.SimpleAmenable.subalphabet_five_generateline 21 - theorem
OAI.SimpleAmenable.universal_subalphabet_five_generateline 40 - theorem
OAI.SimpleAmenable.InitialCoverSystem.geometricSector_five_generateline 50