OAI/NumberTheory/PiExponent/Polynomials/PowerCoverSubstitution.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponent.PowerCover.scaleHomline 11 - theorem
OAI.PiExponent.PowerCover.scaleHom_applyline 16 - theorem
OAI.PiExponent.PowerCover.scale_singleline 19 - theorem
OAI.PiExponent.PowerCover.scale_injectiveline 27 - def
OAI.PiExponent.PowerCover.powerSubstitutionline 35 - theorem
OAI.PiExponent.PowerCover.powerSubstitution_Xline 40 - theorem
OAI.PiExponent.PowerCover.powerSubstitution_eq_mapDomainAlgHomline 44 - theorem
OAI.PiExponent.PowerCover.powerSubstitution_monomialline 54 - theorem
OAI.PiExponent.PowerCover.powerSubstitution_injectiveline 62