OAI/Combinatorics/Chromatic/GradedAlgebra/RationalShearCocycle.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RationalFiber.coefficientUnit line 10
2. def OAI.ElementaryPositivity.RationalFiber.variableUnit line 11
3. lemma OAI.ElementaryPositivity.RationalFiber.coefficientUnit_val line 12
4. lemma OAI.ElementaryPositivity.RationalFiber.variableUnit_val line 13
5. lemma OAI.ElementaryPositivity.RationalFiber.scaleAction_coefficientUnit line 14
6. lemma OAI.ElementaryPositivity.RationalFiber.scaleAction_variableUnit line 18
7. def OAI.ElementaryPositivity.RationalFiber.shearRatio line 23
8. lemma OAI.ElementaryPositivity.RationalFiber.shearRatio_zero line 25
9. lemma OAI.ElementaryPositivity.RationalFiber.shearRatio_add line 26
10. lemma OAI.ElementaryPositivity.RationalFiber.shearRatio_val line 32
11. def OAI.ElementaryPositivity.RationalFiber.reciprocalUnit line 36
12. lemma OAI.ElementaryPositivity.RationalFiber.reciprocalUnit_val line 37
13. lemma OAI.ElementaryPositivity.RationalFiber.reciprocalUnit_scaleAction line 39
14. def OAI.ElementaryPositivity.RationalFiber.oppositeInverseRatio line 49
15. lemma OAI.ElementaryPositivity.RationalFiber.oppositeInverseRatio_zero line 50
16. lemma OAI.ElementaryPositivity.RationalFiber.oppositeInverseRatio_add line 51