OAI/NumberTheory/PiExponent/Polynomials/TranslatedPowerCover.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.TranslatedPowerCover.Ring line 15
2. instance OAI.PiExponent.TranslatedPowerCover.(instance at line 17) line 17
3. def OAI.PiExponent.TranslatedPowerCover.toPolynomial line 20
4. instance OAI.PiExponent.TranslatedPowerCover.(instance at line 23) line 23
5. def OAI.PiExponent.TranslatedPowerCover.decomposition line 27
6. def OAI.PiExponent.TranslatedPowerCover.basis line 43
7. theorem OAI.PiExponent.TranslatedPowerCover.module_free line 47
8. theorem OAI.PiExponent.TranslatedPowerCover.module_finite line 51
9. theorem OAI.PiExponent.TranslatedPowerCover.finrank line 56