OAI/NumberTheory/SiegelZeros/Structure/GradedGeneration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W24.residue_corrections_of_surjective line 17
2. theorem OAI.SiegelZeros.WeightedTorusJets.W24.ideal_power_corrections line 27
3. theorem OAI.SiegelZeros.WeightedTorusJets.W24.ideal_power_preservation line 75
4. def OAI.SiegelZeros.WeightedTorusJets.W24.idealPowerLayerMap line 81
5. theorem OAI.SiegelZeros.WeightedTorusJets.W24.layer_surjective_of_corrections line 86
6. theorem OAI.SiegelZeros.WeightedTorusJets.W24.idealPowerLayerMap_surjective line 101
7. theorem OAI.SiegelZeros.WeightedTorusJets.W24.algebraMap_surjective_of_nilpotent_ideal_layers line 121
8. theorem OAI.SiegelZeros.WeightedTorusJets.W24.ring_length_le_of_residue_and_cotangent line 134