OAI/NumberTheory/PrimePackets/ObservationCovers.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.small_right_chart line 49
2. theorem OAI.PrimeDegreePackets.compact_finite_observation line 68
3. theorem OAI.PrimeDegreePackets.orbit_name_cover_of_reset line 121
4. lemma OAI.PrimeDegreePackets.stepCover_of_matrix_expansion line 206
5. lemma OAI.PrimeDegreePackets.diagonalOneParameter_zero line 233
6. lemma OAI.PrimeDegreePackets.diagonalOneParameter_add line 239
7. lemma OAI.PrimeDegreePackets.diagonalOneParameter_neg line 249
8. lemma OAI.PrimeDegreePackets.diagonalOneParameter_nat line 254
9. lemma OAI.PrimeDegreePackets.diagonal_conjugation_expansion line 262
10. lemma OAI.PrimeDegreePackets.rightAction_iterate line 305
11. lemma OAI.PrimeDegreePackets.rightAction_conjugation line 311
12. lemma OAI.PrimeDegreePackets.rightAction_iterate_conjugation line 318
13. theorem OAI.PrimeDegreePackets.homogeneous_lifted_name_cover line 329
14. lemma OAI.PrimeDegreePackets.conjugation_iterate line 383
15. lemma OAI.PrimeDegreePackets.branch_midpoint_tube line 394
16. lemma OAI.PrimeDegreePackets.rightAction_iterate_measure_preimage line 430
17. theorem OAI.PrimeDegreePackets.lifted_branch_mass line 441