OAI/NumberTheory/SiegelZeros/Structure/Augmentation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W25.constantCoeff_ker_eq_idealOfVars line 18
2. theorem OAI.SiegelZeros.WeightedTorusJets.W25.truncationIdeal_le_constantCoeff_ker line 27
3. def OAI.SiegelZeros.WeightedTorusJets.W25.augmentation line 34
4. theorem OAI.SiegelZeros.WeightedTorusJets.W25.augmentation_mk line 40
5. theorem OAI.SiegelZeros.WeightedTorusJets.W25.augmentation_surjective line 44
6. def OAI.SiegelZeros.WeightedTorusJets.W25.augmentationIdeal line 50
7. theorem OAI.SiegelZeros.WeightedTorusJets.W25.augmentationIdeal_eq_map line 54
8. theorem OAI.SiegelZeros.WeightedTorusJets.W25.idealOfVars_pow_le_truncationIdeal line 60
9. theorem OAI.SiegelZeros.WeightedTorusJets.W25.augmentationIdeal_pow_eq_bot line 75
10. instance OAI.SiegelZeros.WeightedTorusJets.W25.augmentationIdeal_isMaximal line 81
11. theorem OAI.SiegelZeros.WeightedTorusJets.W25.maximal_eq_augmentationIdeal line 85
12. instance OAI.SiegelZeros.WeightedTorusJets.W25.truncatedQuotient_isLocalRing line 99
13. def OAI.SiegelZeros.WeightedTorusJets.W25.augmentationResidueEquiv line 104