OAI/Combinatorics/Chromatic/GradedAlgebra/PureComparisonIdentification.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RationalFiber.laurent_shiftedElementary_zero line 16
2. lemma OAI.ElementaryPositivity.RationalFiber.pureDegree_simple_self line 22
3. lemma OAI.ElementaryPositivity.RationalFiber.completedBiUnit_pure line 26
4. def OAI.ElementaryPositivity.BiTruncation.Through line 49
5. lemma OAI.ElementaryPositivity.BiTruncation.Through.refl line 51
6. lemma OAI.ElementaryPositivity.BiTruncation.Through.symm line 53
7. lemma OAI.ElementaryPositivity.BiTruncation.Through.trans line 55
8. lemma OAI.ElementaryPositivity.BiTruncation.Through.mul line 58
9. lemma OAI.ElementaryPositivity.BiTruncation.Through.conjugate line 69
10. lemma OAI.ElementaryPositivity.BiTruncation.ext line 73
11. lemma OAI.ElementaryPositivity.QuantumTorus.biRegrade_through line 94
12. lemma OAI.ElementaryPositivity.QuantumTorus.oldLaurent_through line 99
13. lemma OAI.ElementaryPositivity.QuantumTorus.oldLaurent_inner_through line 105
14. lemma OAI.ElementaryPositivity.RationalFiber.regrade_congr_through line 137
15. lemma OAI.ElementaryPositivity.RationalFiber.rationalRegrade_congr_through line 145
16. lemma OAI.ElementaryPositivity.RationalFiber.oldUnit_inverse_congr line 152
17. lemma OAI.ElementaryPositivity.RationalFiber.innerHom_coeff_congr line 164
18. lemma OAI.ElementaryPositivity.RationalFiber.comparisonAction_input_congr line 176
19. lemma OAI.ElementaryPositivity.RationalFiber.bounded_action_congr line 191