OAI/Algebra/AlgebraicObstruction/AdicFunctor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.factor_eval line 13
2. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.family line 26
3. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.family_compatible line 31
4. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.map line 41
5. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.eval_map line 46
6. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.map_map line 53
7. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.equiv line 63
8. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicCofinal.equiv_of line 72
9. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.map_pow_le line 88
10. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.quotient line 94
11. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.quotient_compatible line 98
12. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.family line 105
13. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.family_compatible line 109
14. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.map line 119
15. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.eval_map line 123
16. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.map_of line 130