OAI/Algebra/AffineCancellation/Rees.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ComplexCancellation.Rees.Poly line 10
2. def OAI.ComplexCancellation.Rees.xp line 11
3. def OAI.ComplexCancellation.Rees.relation line 12
4. abbrev OAI.ComplexCancellation.Rees.B line 13
5. def OAI.ComplexCancellation.Rees.π line 14
6. def OAI.ComplexCancellation.Rees.q line 15
7. lemma OAI.ComplexCancellation.Rees.relation_zero line 16
8. lemma OAI.ComplexCancellation.Rees.q_regular line 17
9. abbrev OAI.ComplexCancellation.Rees.L line 22
10. def OAI.ComplexCancellation.Rees.c line 23
11. def OAI.ComplexCancellation.Rees.aπ line 24
12. def OAI.ComplexCancellation.Rees.a line 25
13. def OAI.ComplexCancellation.Rees.values line 26
14. def OAI.ComplexCancellation.Rees.eval line 28
15. lemma OAI.ComplexCancellation.Rees.eval_xp line 29
16. lemma OAI.ComplexCancellation.Rees.eval_relation line 36
17. def OAI.ComplexCancellation.Rees.embedding line 53
18. lemma OAI.ComplexCancellation.Rees.embedding_π line 57
19. abbrev OAI.ComplexCancellation.Rees.Bq line 59
20. def OAI.ComplexCancellation.Rees.loc line 60
21. def OAI.ComplexCancellation.Rees.Q line 61
22. lemma OAI.ComplexCancellation.Rees.Q_val line 62
23. lemma OAI.ComplexCancellation.Rees.loc_injective line 63
24. def OAI.ComplexCancellation.Rees.backValues line 67
25. def OAI.ComplexCancellation.Rees.backEval line 69
26. lemma OAI.ComplexCancellation.Rees.backEval_x line 70
27. lemma OAI.ComplexCancellation.Rees.backEval_H line 77
28. def OAI.ComplexCancellation.Rees.backCoefficients line 93
29. lemma OAI.ComplexCancellation.Rees.backCoefficients_aπ line 97
30. def OAI.ComplexCancellation.Rees.backward line 99
31. lemma OAI.ComplexCancellation.Rees.backward_embedding line 105
32. lemma OAI.ComplexCancellation.Rees.embedding_injective line 116
33. instance OAI.ComplexCancellation.Rees.(instance at line 120) line 120
34. instance OAI.ComplexCancellation.Rees.(instance at line 121) line 121