OAI/NumberTheory/PiExponent/Jets/GradedGeneration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentJets.W24.residue_corrections_of_surjective line 12
2. theorem OAI.PiExponentJets.W24.ideal_power_corrections line 22
3. theorem OAI.PiExponentJets.W24.ideal_power_preservation line 68
4. def OAI.PiExponentJets.W24.idealPowerLayerMap line 74
5. theorem OAI.PiExponentJets.W24.layer_surjective_of_corrections line 79
6. theorem OAI.PiExponentJets.W24.idealPowerLayerMap_surjective line 94
7. theorem OAI.PiExponentJets.W24.algebraMap_surjective_of_nilpotent_ideal_layers line 114
8. theorem OAI.PiExponentJets.W24.ring_length_le_of_residue_and_cotangent line 127