OAI/Algebra/AlgebraicObstruction/ScalarCompletion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.quotientEquiv line 15
2. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.quotientEquiv_mk line 22
3. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.quotientEquiv_symm_mk line 27
4. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.quotientEquiv_transition line 32
5. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.quotientEquiv_symm_transition line 42
6. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.equiv line 51
7. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.equiv_of line 74
8. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorEquiv line 81
9. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorEquiv_one_tmul line 87