OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentPureAction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RationalFiber.purePower line 21
2. lemma OAI.ElementaryPositivity.RationalFiber.purePower_eq line 23
3. lemma OAI.ElementaryPositivity.RationalFiber.purePower_commutation line 45
4. lemma OAI.ElementaryPositivity.RationalFiber.purePower_scalar_commute line 55
5. lemma OAI.ElementaryPositivity.RationalFiber.expandedPure_shifted line 62
6. def OAI.ElementaryPositivity.RationalFiber.pureLaurentUnit line 69
7. lemma OAI.ElementaryPositivity.RationalFiber.expand_pure_intertwine line 77
8. lemma OAI.ElementaryPositivity.RationalFiber.expand_pure_conjugate line 103
9. lemma OAI.ElementaryPositivity.RationalFiber.pure_biSupported line 133
10. lemma OAI.ElementaryPositivity.RationalFiber.biRegrade_pure line 143
11. lemma OAI.ElementaryPositivity.RationalFiber.oldLaurent_pure line 157
12. lemma OAI.ElementaryPositivity.RationalFiber.oldLaurent_pure_unit line 161
13. lemma OAI.ElementaryPositivity.RationalFiber.oldLaurent_pure_inverse line 167