OAI/Algebra/FiniteTensor/OffsetEquations.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PD4Tensor.Spreading.independentOffset line 17
2. def OAI.PD4Tensor.Spreading.offsetRetraction line 20
3. def OAI.PD4Tensor.Spreading.graphRetraction line 21
4. theorem OAI.PD4Tensor.Spreading.independentOffset_zero line 24
5. theorem OAI.PD4Tensor.Spreading.offsetRetraction_zero line 29
6. theorem OAI.PD4Tensor.Spreading.graphRetraction_zero line 32
7. theorem OAI.PD4Tensor.Spreading.subst_offsetRetraction_rename line 35
8. theorem OAI.PD4Tensor.Spreading.subst_graphRetraction_rename line 47
9. theorem OAI.PD4Tensor.Spreading.offset_retract line 59
10. theorem OAI.PD4Tensor.Spreading.graph_retract line 73
11. theorem OAI.PD4Tensor.Spreading.independentOffset_injective line 87
12. theorem OAI.PD4Tensor.Spreading.graphRetraction_eq_killCompl line 101
13. theorem OAI.PD4Tensor.Spreading.offset_kernel line 136
14. theorem OAI.PD4Tensor.Spreading.killCompl_mem_jet line 185
15. theorem OAI.PD4Tensor.Spreading.centered_of_jet_close line 198
16. theorem OAI.PD4Tensor.Spreading.exists_offset_relations line 207
17. theorem OAI.PD4Tensor.Spreading.offset_germ_soundness line 237
18. abbrev OAI.PD4Tensor.Spreading.OffsetVariables line 311
19. def OAI.PD4Tensor.Spreading.offsetPoint line 313
20. def OAI.PD4Tensor.Spreading.offsetCoeffHom line 319
21. def OAI.PD4Tensor.Spreading.offsetRelation line 323
22. def OAI.PD4Tensor.Spreading.offsetIdealEquation line 327
23. def OAI.PD4Tensor.Spreading.offsetEquations line 332
24. theorem OAI.PD4Tensor.Spreading.eval_offsetCoeffHom line 337
25. theorem OAI.PD4Tensor.Spreading.eval_offsetRelation line 347
26. theorem OAI.PD4Tensor.Spreading.eval_offsetIdealEquation line 356
27. theorem OAI.PD4Tensor.Spreading.offset_equations_iff line 364
28. theorem OAI.PD4Tensor.Spreading.offset_point_solves line 377
29. theorem OAI.PD4Tensor.Spreading.finite_offset_presentation line 399
30. theorem OAI.PD4Tensor.Spreading.algebraic_germ_artin line 446