OAI/NumberTheory/PiExponent/Geometry/FiniteNormalizationGrowth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentJets.W29.boundedCoefficientMap line 21
2. def OAI.PiExponentJets.W29.generatorPiece line 28
3. lemma OAI.PiExponentJets.W29.mem_generatorPiece line 33
4. lemma OAI.PiExponentJets.W29.generatorPiece_mono line 44
5. instance OAI.PiExponentJets.W29.generatorPiece_finite line 50
6. lemma OAI.PiExponentJets.W29.finrank_generatorPiece_le line 55
7. lemma OAI.PiExponentJets.W29.mul_mem_generatorPiece line 68
8. theorem OAI.PiExponentJets.W29.finite_multiplication_matrices line 99
9. lemma OAI.PiExponentJets.W29.variable_pow_mem_generatorPiece line 144
10. lemma OAI.PiExponentJets.W29.monomial_mem_generatorPiece line 159
11. lemma OAI.PiExponentJets.W29.polynomial_mem_generatorPiece line 185
12. theorem OAI.PiExponentJets.W29.finite_normalization_upper_growth line 206