OAI/Combinatorics/Chromatic/GradedAlgebra/NonpRegradeFaithful.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.FullHomogeneous line 18
2. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_coeff_eval line 21
3. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_read line 29
4. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_injective_homogeneous line 47
5. lemma OAI.ElementaryPositivity.QuantumTorus.torus_neg_one_mul line 75
6. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.invOfUnit line 79
7. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_one line 113
8. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_zero line 118
9. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_one line 123
10. def OAI.ElementaryPositivity.QuantumTorus.boundedRegradeSubring line 134
11. def OAI.ElementaryPositivity.QuantumTorus.regradeHom line 142
12. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_inverse_mul line 149
13. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_mul_inverse line 154