OAI/NumberTheory/SiegelZeros/LocalAlgebra/RingLength.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.W24.filtrationRestriction line 17
2. def OAI.SiegelZeros.WeightedTorusJets.W24.filtrationLayerMap line 22
3. theorem OAI.SiegelZeros.WeightedTorusJets.W24.correction_of_layer_surjective line 31
4. theorem OAI.SiegelZeros.WeightedTorusJets.W24.surjective_of_finite_corrections line 45
5. theorem OAI.SiegelZeros.WeightedTorusJets.W24.surjective_of_finite_layers line 65
6. theorem OAI.SiegelZeros.WeightedTorusJets.W24.length_le_of_finite_layers line 76
7. theorem OAI.SiegelZeros.WeightedTorusJets.W24.scalar_lift_difference line 91
8. theorem OAI.SiegelZeros.WeightedTorusJets.W24.ring_length_le_of_finite_layers line 109