OAI/NumberTheory/SiegelZeros/Structure/IdentityHeight.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W58.identityEvaluation_surjective line 15
2. def OAI.SiegelZeros.W58.identityIdeal line 20
3. instance OAI.SiegelZeros.W58.identityIdeal_isMaximal line 22
4. theorem OAI.SiegelZeros.W58.mem_identityIdeal line 25
5. theorem OAI.SiegelZeros.W58.coordinate_sub_one_mem_identityIdeal line 28
6. theorem OAI.SiegelZeros.W58.torus_zero_ne_one line 31
7. abbrev OAI.SiegelZeros.W58.IdentityLocalRing line 36
8. def OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.polynomialIdentityEvaluation line 48
9. def OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.polynomialIdentityIdeal line 51
10. lemma OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.polynomialIdentityEvaluation_surjective line 54
11. instance OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.polynomialIdentityIdeal_isMaximal line 59
12. def OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.stepEvaluation line 63
13. lemma OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.stepEvaluation_surjective line 66
14. lemma OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.polynomialIdentityEvaluation_succ line 70
15. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.polynomialIdentityIdeal_height line 81
16. lemma OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.identityIdeal_comap_polynomial line 120
17. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.identityIdeal_height line 128
18. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.prime_ne_identity_of_height_le_three line 133
19. theorem OAI.SiegelZeros.WeightedTorusJets.IdentityHeight.not_identity_contained_of_height_le_three line 139