OAI/NumberTheory/PiExponent/Polynomials/PowerCoverBasis.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.PowerCover.decompositionAddEquiv line 10
2. theorem OAI.PiExponent.PowerCover.decompositionAddEquiv_monomial line 17
3. theorem OAI.PiExponent.PowerCover.decompositionAddEquiv_power_mul line 24
4. def OAI.PiExponent.PowerCover.PowerModule line 42
5. instance OAI.PiExponent.PowerCover.(instance at line 44) line 44
6. def OAI.PiExponent.PowerCover.toPolynomial line 47
7. instance OAI.PiExponent.PowerCover.powerAlgebra line 50
8. theorem OAI.PiExponent.PowerCover.toPolynomial_smul line 55
9. def OAI.PiExponent.PowerCover.decomposition line 60
10. def OAI.PiExponent.PowerCover.basis line 66
11. theorem OAI.PiExponent.PowerCover.basis_toPolynomial line 70
12. theorem OAI.PiExponent.PowerCover.module_free line 78
13. theorem OAI.PiExponent.PowerCover.module_finite line 82
14. theorem OAI.PiExponent.PowerCover.finrank line 87
15. instance OAI.PiExponent.PowerCover.(instance at line 96) line 96