OAI/Algebra/AffineCancellation/ReesReduction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ComplexCancellation.Rees.redValues line 10
2. def OAI.ComplexCancellation.Rees.redEval line 12
3. lemma OAI.ComplexCancellation.Rees.redEval_relation line 13
4. def OAI.ComplexCancellation.Rees.red line 18
5. lemma OAI.ComplexCancellation.Rees.red_π line 22
6. lemma OAI.ComplexCancellation.Rees.red_q line 23
7. abbrev OAI.ComplexCancellation.Rees.Special line 24
8. def OAI.ComplexCancellation.Rees.ρ line 25
9. def OAI.ComplexCancellation.Rees.backRedValues line 26
10. def OAI.ComplexCancellation.Rees.backRedEval line 28
11. lemma OAI.ComplexCancellation.Rees.ρ_q line 29
12. lemma OAI.ComplexCancellation.Rees.backRedEval_relation line 30
13. def OAI.ComplexCancellation.Rees.backRed line 38
14. lemma OAI.ComplexCancellation.Rees.backRed_π line 43
15. lemma OAI.ComplexCancellation.Rees.backRed_red line 45
16. lemma OAI.ComplexCancellation.Rees.red_zero_iff line 54
17. lemma OAI.ComplexCancellation.Rees.q_not_isUnit line 64
18. lemma OAI.ComplexCancellation.Rees.maximum_q_factor line 70