OAI/GroupTheory/SimpleAmenable/CentralCovers/StarProjection.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SimpleAmenable.formalPolygonTableline 15 - theorem
OAI.SimpleAmenable.formalPolygonTable_wholeline 19 - theorem
OAI.SimpleAmenable.formalPolygonTable_testline 28 - theorem
OAI.SimpleAmenable.formalPolygonTable_eq_oneline 36 - theorem
OAI.SimpleAmenable.actualStar_eval_projectionline 44 - theorem
OAI.SimpleAmenable.InitialCoverSystem.pairStar_projectionline 72 - theorem
OAI.SimpleAmenable.InitialCoverSystem.pairStar_subfamily_memline 86 - theorem
OAI.SimpleAmenable.InitialCoverSystem.pairStar_subfamily_localline 112 - theorem
OAI.SimpleAmenable.InitialCoverSystem.pair_actual_centralline 163 - theorem
OAI.SimpleAmenable.InitialCoverSystem.pair_actual_lawline 213