OAI/Algebra/AlgebraicObstruction/AnalyticReducedness.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.reduced_tensor_of_field_embeddings line 23
2. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.reduced_flat_domain_tensor line 47
3. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.reduced_finite_domain_completion line 66
4. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.reduced_domain_point_completion line 90
5. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.reduced_completion_of_quotients line 119
6. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.reduced_top_completion line 150
7. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.reduced_point_completion line 164
8. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.level line 208
9. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.level_factor line 211
10. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.family line 217
11. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.compatible line 221
12. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.forward line 229
13. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.eval_forward line 232
14. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.inverseFamily line 237
15. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.inverse_compatible line 241
16. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.inverse line 252
17. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.eval_inverse line 255
18. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.equiv line 260
19. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionLocalization.equiv_of line 280
20. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.radical_map_completion line 295
21. instance OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.rationalPointPrime line 316
22. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.radical_local_completion_transfer line 319
23. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AnalyticReducedness.radical_local_completion line 344