OAI/NumberTheory/Ostmann/Arithmetic/IncidenceComponents.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.IncidenceHaar.Component line 11
2. instance OAI.Ostmann.Arithmetic.IncidenceHaar.componentFintype line 14
3. instance OAI.Ostmann.Arithmetic.IncidenceHaar.componentDecidableEq line 16
4. def OAI.Ostmann.Arithmetic.IncidenceHaar.componentLabel line 19
5. def OAI.Ostmann.Arithmetic.IncidenceHaar.componentRoot line 22
6. theorem OAI.Ostmann.Arithmetic.IncidenceHaar.componentRoot_label line 25
7. theorem OAI.Ostmann.Arithmetic.IncidenceHaar.componentPath line 29
8. theorem OAI.Ostmann.Arithmetic.IncidenceHaar.componentLabel_edge line 35
9. def OAI.Ostmann.Arithmetic.IncidenceHaar.balanced line 39
10. theorem OAI.Ostmann.Arithmetic.IncidenceHaar.boundary_range_eq_balanced line 45
11. def OAI.Ostmann.Arithmetic.IncidenceHaar.boundaryToBalanced line 57
12. theorem OAI.Ostmann.Arithmetic.IncidenceHaar.boundaryToBalanced_surjective line 62
13. instance OAI.Ostmann.Arithmetic.IncidenceHaar.balancedFintype line 71
14. theorem OAI.Ostmann.Arithmetic.IncidenceHaar.boundary_uniform line 74